Synthesis of Communicating Processes from Temporal Logic Specifications

Abstract

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.