Synthesis of Concurrent Systems with Many Similar Processes

Paul C. Attie, E. Allen Emerson

Research output: Contribution to journalArticle

45 Scopus citations

Abstract

Methods for synthesizing concurrent programs from temporal logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson and Clarke and by Manna and Wolper. An important advantage of these synthesis methods is that they obviate the need to manually compose a program and manually construct a proof of its correctness. One only has to formulate a precise problem specification; the synthesis method then mechanically constructs a correct solution. A serious drawback of these methods in practice, however, is that they suffer from the state explosion problem. To synthesize a concurrent system consisting of K sequential processes, each having N states in its local transition diagram, requires construction of the global product-machine having about NK global states in general. This exponential growth in K makes it infeasible to synthesize systems composed of more than 2 or 3 processes. In this article, we show how to synthesize concurrent systems consisting of many (i.e., a finite but arbitrarily large number K of) similar sequential processes. Our approach avoids construction of the global product-machine for K processes; instead, it constructs a two-process product-machine for a single pair of generic sequential processes. The method is uniform in K, providing a simple template that can be instantiated for each process to yield a solution for any fixed K. The method is also illustrated on synchronization problems from the literature.

Original languageEnglish (US)
Pages (from-to)51-115
Number of pages65
JournalACM Transactions on Programming Languages and Systems
Volume20
Issue number1
DOIs
StatePublished - Jan 1998
Externally publishedYes

Keywords

  • C.2.4 [Computer-Communication Networks]: Distributed Systems
  • D.1.2 [Programming Techniques]: Automatic Programming
  • D.1.3 [Programming Techniques]: Concurrent Programming
  • D.2.4 [Software Engineering]: Program Verification

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Synthesis of Concurrent Systems with Many Similar Processes'. Together they form a unique fingerprint.

  • Cite this