Specification and synthesis of communicating processes using an extended temporal logic
Pierre Wolper · 1982
We apply an Extended Propositional Temporal Logic (EPTL) to the specification and synthesis of the synchronization part of communicating processes. To specify a process, we give an EPTL formula that describes its sequence of communications. The synthesis is done by constructing a model of the given specifications using a tableau-like satisfiability algorithm for the extended temporal logic. This model can then be interpreted as a program.