In [1,2], we present a method for the synthesis of finite-state concurrent programs from specifications expressed in the branching-time propositional temporal logic CTL [8]. This method avoids exhaustive state-space search. Rather than deal with the behavior of the program as a whole, the method instead generates the interactions between processes one pair at a time. Thus, for every pair of processes that interact, a pair-machine is constructed that gives their interaction. Since the pair-machines are small (), they can be built using exhaustive methods. A pair-program can then be extracted from the pair-machine. This extraction operation takes every transition of the pair-machine and realizes it as a piece of code in the pair-program [2,9]. The final synthesized program is generated by a syntactic composition of all the pair-programs. This composition has a conjunctive nature: a process can execute a transition if and only if that transition is permitted by every pair-program in which participates. Thus, two pair-programs which have no processes in common do not interact directly. Two pair-programs that do have a process in common will interact via : the pair-programs in effect must synchronize whenever makes a transition, so that the transition is executed in both pair-programs simultaneously. For example, if , , and are three pair-programs which all implement a two-process mutual exclusion algorithm, then they can be composed as discussed above into a single program which implements three-process mutual exclusion. In this program, when wishes to access the critical section, it must be permitted to do so by both (as per the pair-program) and by (as per the pair-program).
Due to the complexity of the synthesis and verification problems for finite-state concurrent programs, any efficient synthesis method is necessarily incomplete: it may fail to produce a program that satisfies a given specification even though such a program exists. In the synthesis method of [1,2], the incompleteness takes the form of two technical assumptions that the pair-programs must satisfy in order for the synthesized program to be correct. One technical assumption requires that after a process executes, either it can execute again (i.e., is enabled), or it does not block any other process. This prevents deadlock. The other technical assumption requires that a process cannot forever block another process if the second process must make progress in order to satisfy a liveness property in the specification. This guarantees liveness.
We refer the reader to [1,2] for examples of synthesis of solutions to the following problems, all for an arbitrarily large number of processes: -process mutual exclusion, dining philosophers, drinking philosophers [5], -out-of- mutual exclusion, and two-phase commit.