Synthesis of Communicating Processes from Temporal Logic Specifications

in ACM Transactions on Programming Languages & Systems (1984), 6(1), 68-93

In this paper, Propositional Temporal Logic (PTL) is applied to the specification and synthesis of the synchronization part of communicating processes. To specify a process, a PTL formula that describes ... [more ▼]

In this paper, Propositional Temporal Logic (PTL) is applied to the specification and synthesis of the synchronization part of communicating processes. To specify a process, a PTL formula that describes its sequence of communications is given. The synthesis is done by constructing a model of the given specifications using a tableau-like satisfiability algorithm for PTL. This model can then be interpreted as a program. [less ▲]