Specification and synthesis of communicating processes using an extended temporal logic: (preliminary version)

ABSTRACT

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.

REFERENCES

• 1: Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567551]
• 2: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 3: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• 4: {Gr75} P. Griffiths, "SYNVER: A System for the Automatic Synthesis and Verification and Synthesis of Synchronization Processes", Ph. D. Thesis, Harvard University, June 1975.
• 5: {Ha75} A. N. Habermann, "Path Expressions", Computer Science Report, Carnegie-Mellon University, 1975.
• 6: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 7: {La78} M. Laventhal, "Synthesis of Synchronization Code for Data Abstractions", Ph. D. Thesis, MIT, June 1978.
• 8: {MP81} Z. Manna, A. Pnueli, "Verification of Concurrent Programs: the Temporal Framework", The Correctness Problem in Computer Science (R. S. Boyer and J S. Moore, eds.), International Lecture Series in Computer Science, Academic Press, London, 1981.
• 9: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, Logic of Programs, Workshop, p.253-281, May 01, 1981
• 10: {Pn77} A. Pnueli, "The Temporal Logic of Programs", Proceedings of the Eighteenth Symposium on Foundations of Computer Science, Providence, RI, November 1977, pp. 46--57.
• 11: {Pr67} A. Prior, Past, Present and Future, Oxford University Press, 1967.
• 12: {RU71} N. Rescher, A. Urquart, Temporal Logic, Springer-Verlag, 1971
• 13: {RK81} K. Ramamritham, R. M. Keller, "Specification and Synthesis of Synchronizers", Proceedings International Symposium on Parallel Processing, August 1980, pp. 311--321.
• 14: {Sm68} R. M. Smullyan, First Order Logic, Springer-Verlag, Berlin, 1968.
• 15: {Wo81} P. Wolper, "Temporal Logic Can Be More Expressive", Proceedings of the Twenty-Second Symposium on Foundations of Computer Science, Nashville, TN, October 1981.