@inproceedings{9c0761c6773c4174936ed7da8dd02de6,
title = "Synthesis of concurrent systems with many similar sequential processes",
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.",
author = "Attie, {Paul C.} and Emerson, {E. Allen}",
year = "1989",
month = dec,
day = "1",
language = "English (US)",
isbn = "0897912942",
series = "Conf Rec Sixteenth Annu ACM Symp Princ Program Lang",
publisher = "Publ by ACM",
pages = "191--201",
booktitle = "Conf Rec Sixteenth Annu ACM Symp Princ Program Lang",
note = "Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages ; Conference date: 11-01-1989 Through 13-01-1989",
}