Synthesis of Communicating Processes from Temporal Logic Specifications
- 1 January 1984
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 6 (1) , 68-93
- https://doi.org/10.1145/357233.357237
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.Keywords
This publication has 6 references indexed in Scilit:
- Communicating sequential processesCommunications of the ACM, 1978
- Path ExpressionsPublished by Defense Technical Information Center (DTIC) ,1975
- SYNVERPublished by Association for Computing Machinery (ACM) ,1974
- Temporal LogicPublished by Springer Nature ,1971
- First-Order LogicPublished by Springer Nature ,1968
- Past, Present and FuturePublished by Oxford University Press (OUP) ,1967