More Web Proxy on the site http://driver.im/

Article

Free access

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

Author:

Pierre WolperAuthors Info & Claims

POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 20 - 33

https://doi.org/10.1145/582153.582156

Published: 25 January 1982 Publication History

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]

{BMP81} M. Ben-Ari, Z. Manna, A. Pnueli, "The Logic of Nexttime", Eighth ACM Symposium on Principles of Programming Languages, Williamsburg, VA, January 1981, pp. 164--176.

Digital Library

[2]

{CE81} E. M. Clarke, E. A. Emerson, "Synthesis of Synchronization Skeletons from Branching Time Temporal Logic", Proceedings of the Workshop on Logics of Programs, Yorktown-Heights, NY, Springer-Verlag Lecture Notes in Computer Science, 1981

Digital Library

[3]

{GPSS80} D. Gabbay, A. Pnueli, S. Shelah and J. Stavi, "The Temporal Analysis of Fairness", Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, NV, January 1980, pp. 163--173.

Digital Library

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

{Ho78} C. A. R. Hoare, "Communicating Sequential Processes", Communications of the ACM, Vol. 21, No 8 (August 1978), pp. 666--677.

Digital Library

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

Digital Library

[9]

{MW} Z. Manna, P. Wolper, "Synthesis of Communicating Processes from Temporal Logic Specifications", Proceedings of the Workshop on Logics of Programs, Yorktown-Heights, NY, Springer-Verlag Lecture Notes in Computer Science, 1981

Digital Library

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

Cited By

Bansal SNamjoshi KSa'ar Y(2019)Synthesis of coordination programs from linear temporal specificationsProceedings of the ACM on Programming Languages10.1145/33711224:POPL(1-27)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371122
Landauer C(2017)Mitigating the Inevitable Failure of Knowledge Representation2017 IEEE International Conference on Autonomic Computing (ICAC)10.1109/ICAC.2017.32(239-246)Online publication date: Jul-2017
https://doi.org/10.1109/ICAC.2017.32
Moszkowski B(2012)A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite TimeJournal of Applied Non-Classical Logics10.3166/jancl.14.55-10414:1-2(55-104)Online publication date: 13-Apr-2012
https://doi.org/10.3166/jancl.14.55-104
Show More Cited By

Recommendations

Constructive linear-time temporal logic: Proof systems and Kripke semantics

In this paper we study a version of constructive linear-time temporal logic (LTL) with the ''next'' temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time ...
Specification of distributed programs using temporal interval logic
Specification of communicating processes: temporal logic versus refusals-based refinement
Abstract
In this paper we consider the relationship between refinement-oriented specification and specifications using a temporal logic. We investigate the extent to which one can check whether a program in a process algebra, such as Communicating ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '82: Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1982

378 pages

ISBN:0897910656

DOI:10.1145/582153

Conference Chair:
Richard DeMillo

Copyright © 1982 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 1982

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

POPL '82 Paper Acceptance Rate 38 of 121 submissions, 31%;

Overall Acceptance Rate 800 of 4,009 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
370
Total Downloads

Downloads (Last 12 months)43
Downloads (Last 6 weeks)7

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bansal SNamjoshi KSa'ar Y(2019)Synthesis of coordination programs from linear temporal specificationsProceedings of the ACM on Programming Languages10.1145/33711224:POPL(1-27)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371122
Landauer C(2017)Mitigating the Inevitable Failure of Knowledge Representation2017 IEEE International Conference on Autonomic Computing (ICAC)10.1109/ICAC.2017.32(239-246)Online publication date: Jul-2017
https://doi.org/10.1109/ICAC.2017.32
Moszkowski B(2012)A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite TimeJournal of Applied Non-Classical Logics10.3166/jancl.14.55-10414:1-2(55-104)Online publication date: 13-Apr-2012
https://doi.org/10.3166/jancl.14.55-104
Moszkowski B(2012)A Complete Axiom System for Propositional Interval Temporal Logic with Infinite TimeLogical Methods in Computer Science10.2168/LMCS-8(3:10)20128:3Online publication date: 13-Aug-2012
https://doi.org/10.2168/LMCS-8(3:10)2012
Klüppelholz SBaier C(2010)Alternating-time stream logic for multi-agent systemsScience of Computer Programming10.1016/j.scico.2009.07.00775:6(398-425)Online publication date: 1-Jun-2010
https://dl.acm.org/doi/10.1016/j.scico.2009.07.007
Kiam Tian Seow Manh Tung Pham Chuan Ma Yokoo M(2009)Coordination Planning: Applying Control Synthesis Methods for a Class of Distributed AgentsIEEE Transactions on Control Systems Technology10.1109/TCST.2008.92457417:2(405-415)Online publication date: Mar-2009
https://doi.org/10.1109/TCST.2008.924574
Bjørner NHendrix J(2009)Linear Functional Fixed-pointsProceedings of the 21st International Conference on Computer Aided Verification10.1007/978-3-642-02658-4_13(124-139)Online publication date: 23-Jun-2009
https://dl.acm.org/doi/10.1007/978-3-642-02658-4_13
Klüppelholz SBaier C(2008)Alternating-time stream logic for multi-agent systemsProceedings of the 10th international conference on Coordination models and languages10.5555/1788954.1788966(184-198)Online publication date: 4-Jun-2008
https://dl.acm.org/doi/10.5555/1788954.1788966
Niz D(2008)Architectural Concurrency Equivalence with Chaotic ModelsProceedings of the 2008 5th International Workshop on Model-based Methodologies for Pervasive and Embedded Software10.1109/MOMPES.2008.10(57-67)Online publication date: 5-Apr-2008
https://dl.acm.org/doi/10.1109/MOMPES.2008.10
Klüppelholz SBaier C(2008)Alternating-Time Stream Logic for Multi-agent SystemsCoordination Models and Languages10.1007/978-3-540-68265-3_12(184-198)Online publication date: 2008
https://doi.org/10.1007/978-3-540-68265-3_12
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents