Synthesis of large dynamic concurrent programs from dynamic specifications

We present two methods for synthesizing large concurrent programs from temporal logic specifications. The first method deals with finite-state concurrent programs that are static, i.e., the set of processes is fixed. It produces an infinite family of static finite-state concurrent programs. The second method deals with dynamic concurrent programs, i.e., new processes can be created and added at run-time. It produces a single dynamic concurrent program. A dynamic concurrent program may be viewed as a limiting case of an infinite family of static programs, and so the second method may be viewed as generalizing the first. Our methods are algorithmically efficient, with complexity polynomial in the number of component processes (of the program) that are “alive” at any time. We do not explicitly construct the automata-theoretic product of all processes that are alive, thereby avoiding state explosion. Instead, for each interacting pair of processes, we construct (from a pair-specification) a pair-structure which embodies the interaction of the two processes. From each pair-structure, we synthesize a pair-program to coordinate the two processes. Our second method allows pair-programs to be added dynamically at run-time. They are then “composed conjunctively” with the currently alive pair-programs to “re-synthesize” the program. We can thus add new behaviors, which result in new properties being satisfied, at run-time. This “incremental composition” step has complexity independent of the total number of processes; it only requires the mechanical analysis of the two processes in the pair-program, and their immediate neighbors, i.e., the other processes which they interact directly with. Thus, any state-explosion incurred is explosion in the product of only two processes. We establish “large model” theorems which show that the synthesized global program inherits correctness properties from the pair-programs.