Synthesis of Communicating Processes from Temporal Logic Specifications
Zohar Manna, Pierre Wolper · ACM Transactions on Programming Languages and Systems · 1984
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.