Synthesis of concurrent systems with many similar sequential processes

Paul C. Attie, E. Allen Emerson

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

11 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. 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. A serious drawback of these methods in practice, however, is that they suffer from the state explosion problem. 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)
Title of host publicationConf Rec Sixteenth Annu ACM Symp Princ Program Lang
PublisherPubl by ACM
Pages191-201
Number of pages11
ISBN (Print)0897912942
StatePublished - Dec 1 1989
Externally publishedYes
EventConference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages - Austin, TX, USA
Duration: Jan 11 1989Jan 13 1989

Publication series

NameConf Rec Sixteenth Annu ACM Symp Princ Program Lang

Conference

ConferenceConference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages
CityAustin, TX, USA
Period1/11/891/13/89

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint Dive into the research topics of 'Synthesis of concurrent systems with many similar sequential processes'. Together they form a unique fingerprint.

  • Cite this

    Attie, P. C., & Emerson, E. A. (1989). Synthesis of concurrent systems with many similar sequential processes. In Conf Rec Sixteenth Annu ACM Symp Princ Program Lang (pp. 191-201). (Conf Rec Sixteenth Annu ACM Symp Princ Program Lang). Publ by ACM.