SYNTHESIS OF CONCURRENT SYSTEMS WITH MANY SIMILAR PROCESSES

Methods for synthesizing concurrent programs from temporal logic speci fications based on the use of a decision procedure for testing tempora l 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 cons truct a proof of its correctness. One only has to formulate a precise problem specification; the synthesis method then mechanically construc ts a correct solution. A serious drawback of these methods in practice , however, is that they suffer from the state explosion problem. To sy nthesize a concurrent system consisting of K sequential processes, eac h having N states in its local transition diagram, requires constructi on of the global product-machine having about N-K global states in gen eral. This exponential growth in K makes it infeasible to synthesize s ystems composed of more than 2 or 3 processes. In this article, we sho w how to synthesize concurrent systems consisting of many (i.e., a fin ite but arbitrarily large number K of) similar sequential processes. O ur approach avoids construction of the global product-machine for K pr ocesses; instead, it constructs a two-process product-machine for a si ngle 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 o n synchronization problems from the literature.