Synthesis of large concurrent programs via pairwise composition

We present a tractable method for synthesizing arbitrarily large concurrent programs from specifications expressed in temporal logic. Our method does not explicitly construct the global state transition diagram of the program to be synthesized, and thereby avoids state explosion. Instead, it constructs a state transition diagram for each pair of component processes (of the program) that interact. This "pair-program" embodies all possible interactions of the two processes. Our method proceeds in two steps. First, we construct a pair-program for every pair of "connected" processes, and analyze these pair-programs for desired correctness properties. We then take the "pair processes" of the pair-programs, and "compose" them in a certain way to synthesize the large concurrent program. We establish a "large model" theorem which shows that the synthesized large program inherits correctness properties from the pair-programs.