Synthesis of large concurrent programs via pairwise composition

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Scopus citations

Abstract

We present a tractable method for synthesizing arbitrarily large concurrent programs from specifications expressed in temporal logic. Our method does not explicitly construct the global state transition diagram of the program to be synthesized, and thereby avoids state explosion. Instead, it constructs a state transition diagram for each pair of component processes (of the program) that interact. This "pair-program" embodies all possible interactions of the two processes. Our method proceeds in two steps. First, we construct a pair-program for every pair of "connected" processes, and analyze these pair-programs for desired correctness properties. We then take the "pair processes" of the pair-programs, and "compose" them in a certain way to synthesize the large concurrent program. We establish a "large model" theorem which shows that the synthesized large program inherits correctness properties from the pair-programs.

Original languageEnglish (US)
Title of host publicationCONCUR 1999, Concurrency Theory - 10th International Conference, Proceedings
PublisherSpringer Verlag
Pages130-145
Number of pages16
ISBN (Print)3540664254, 9783540664253
DOIs
StatePublished - 1999
Externally publishedYes
Event10th International Conference on Concurrency Theory, CONCUR 1999 - Eindhoven, Netherlands
Duration: Aug 24 1999Aug 27 1999

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1664 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference10th International Conference on Concurrency Theory, CONCUR 1999
Country/TerritoryNetherlands
CityEindhoven
Period8/24/998/27/99

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Synthesis of large concurrent programs via pairwise composition'. Together they form a unique fingerprint.

Cite this