Synthesis of Communicating Processes from Temporal Logic Specifications

Manna, Zohar; Wolper, Pierre

doi:10.1145/357233.357237

Request a copy

Article (Scientific journals)

Synthesis of Communicating Processes from Temporal Logic Specifications

Manna, Zohar; Wolper, Pierre

1984 • In ACM Transactions on Programming Languages and Systems, 6 (1), p. 68-93

Peer Reviewed verified by ORBi

Permalink
https://hdl.handle.net/2268/116690

DOI
10.1145/357233.357237

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

toplas84.pdf

Publisher postprint (1.45 MB)

Request a copy

All documents in ORBi are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

Temporal logic; Program synthesis; Synchronization; Mutual exclusion; Concurrency

Abstract :

[en] 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.

Disciplines :

Computer science

Author, co-author :

Manna, Zohar; Stanford University > Department of Computer Science

Wolper, Pierre ; Université de Liège - ULiège > Département d'electricité, électronique et informatique (Institut Montefiore)

Language :

English

Title :

Synthesis of Communicating Processes from Temporal Logic Specifications

Publication date :

1984

Journal title :

ACM Transactions on Programming Languages and Systems

ISSN :

0164-0925

eISSN :

1558-4593

Publisher :

Association for Computing Machinery, New York, United States - New York

Volume :

Issue :

Pages :

68-93

Peer reviewed :

Peer Reviewed verified by ORBi

Available on ORBi :

since 16 April 2012

Statistics

Number of views

59 (0 by ULiège)

Number of downloads

0 (0 by ULiège)

More statistics

Scopus citations^®

272

Scopus citations^®
without self-citations

261

OpenCitations

289

Bibliography

BEN-ARI, M., MANNA, Z., AND PNEULI, A. The temporal logic of branching time. In Proceedings 8th ACM Symposium on Principles on Programming Languages (Williamsburg, Va., Jan. 26-28), ACM, New York, 1981, pp. 164-176.
CLARKE, E. M., AND EMERSON, E.A. Synthesis of synchronization skeletons from branching time temporal logic. In Proceedings of the Workshop on Logics of Programs (Yorktown-Heights, N.Y.). Lecture Notes in Computer Science, Springer-Verlag, New York, 1981, pp. 52-71.
GABBAY, D., PNEULI, A., SHELAH, S., AND STAVI, J. On the temporal analysis of fairness. In Proceedings 7th ACM Symposium on Principles of Programming Languages (Las Vegas, Nev., Jan. 28-30), ACM, New York, 1980, pp. 163-173.
GRIFFITHS, P. SYNVER: A system for the automatic synthesis and verification and synthesis of synchronization processes. Ph.D. dissertation, Aiken Computation Laboratory, Harvard Univ., Cambridge, Mass., June 1975.
HABERMANN, A.N. Path expressions. Computer Science Report, Carnegie-Mellon University, Pittsburgh, Pa., 1975.
HOARE, C. A. R. Communicating sequential processes. Commun. ACM 21, 8 (Aug. 1978), 666-677.
LAVENTHAL, M. Synthesis of synchronization code for data abstractions. Ph.D. dissertation, Laboratory for Computer Science, Massachusetts Institute of Technology, Boston, Mass., June 1978.
MANNA, Z., AND PNEULI, I. Verification of concurrent programs: the temporal framework. In The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore (eds.). International Lecture Series in Computer Science. Academic Press, New York, 1981, pp. 215-273.
PNEULI, A. The temporal logic of programs. In Proceedings of the 18th Symposium on Foundations of Computer Science (Providence, R.I., Nov.) 1977, pp. 46-57.
PRIOR, A. Past, Present and Future. Oxford University Press, New York, 1967.
RAMAMRITHAM, K., AND KELLER, R. M. Specification and synthesis of synchronizers. In Proceedings International Symposium on Parallel Processing (Aug.) 1980, pp. 311-321.
RESCHER, N., AND URQUART, A. Temporal Logic, Springer-Verlag, New York, 1971.
SMULLYAN, R.U. First Order Logic. Springer-Verlag, New York, 1968.
WOLPER, P. Specification and synthesis of communicating processes using an extended temporal logic. In Proceedings of 9th ACM Symposium on Principles of Programming Languages (Albuquerque, N.M., Jan. 25-27), ACM, New York, 1982, pp. 20-33.
WOLPER, P. Temporal logic can be more expressive. In Proceedings of the 22d Symposium on Foundations of Computer Science (Nashville, Tenn., Oct.), 1981.