Article

Free access

Modalities for model checking (extended abstract): branching time strikes back

Authors:

E. Allen Emerson,

Chin-Laung LeiAuthors Info & Claims

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

Pages 84 - 96

https://doi.org/10.1145/318593.318620

Published: 01 January 1985 Publication History

First page of PDF

References

[1]

{AE83} Antila, M., Erikkson, H., Ikonen, J., Kujansuu, R., Ojala, L., Tuominen, H., Tools and Studies of Formal Techniques - Petri Nets and Temporal Logic, Protocol Specification, Testing, and Verification III, H. Rudin and C. West (editors), Elsevier North-Holland, IFIP, 1983.

[2]

{AB80} Abrahamson, K., Decidability and Expressiveness of Logics of Processes, PhD Thesis, University of Washington, 1980.

Digital Library

[3]

{BSW69} Bartlet, K, Scantlebury, R., and Wilkinson, P., A Note on Reliable Full-Duplex Transmission over Half-Duplex Links, Comm. of the ACM, vol. 12, no. 5, pp. 260-261, 1969.

Digital Library

[4]

{CE81} Clarke, E. M., Emerson, E. A., Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic, IBM Logics of Programs Workshop, Springer LNCS #131, pp. 52-71, May 1981.

Digital Library

[5]

{CES83} Clarke, E. M., Emerson, E. A., and Sistla, A. P., Automatic Verification of Finite State Concurrent System Using Temporal Logic, 10th Annual ACM 10th Annual ACM Symp. on Principles of Programming Languages, 1983.

Digital Library

[6]

{CM83} Clarke, E. M., Mishra, B., Automatic Verification of Asynchronous Circuits, CMU Logics of Programs Workshop, Springer LNCS #164, pp. 101-115, May 1983.

Digital Library

[7]

{EC80} Emerson, E. A., and Clarke, E. M., Characterizing Correctness Properties of Parallel Programs as Fixpoints. Proc. 7th Int. Colloquium on Automata, Languages, and Programming, Lecture Notes in Computer Science #85, Springer-Verlag, 1981.

Digital Library

[8]

{EC82} Emerson, E. A., and Clarke, E. M., Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons, Tech. Report TR-208, Univ. of Texas, 1982.

[9]

{EH82} Emerson, E. A., and Halpern, J. Y., Decision Procedures and Expressiveness in the Temporal Logic of Branching Time, 14th Annual ACM Symp. on Theory of Computing, 1982.

Digital Library

[10]

{EH83} Emerson, E. A., and Halpern, J. Y., 'Sometimes' and 'Not Never' Revisited: On Branching versus Linear Time 10th Annual ACM Symp. on Principles of Programming Languages, January 1983.

Digital Library

[11]

{ES84} Emerson, E. A., and Sistla, A. P., Deciding Branching Time Logic, 16 Annual ACM Symp. on Theory of Computing, 1984.

Digital Library

[12]

{FL79} Fischer, M. J., and Ladner, R. E, Propositional Dynamic Logic of Regular Programs, JCSS vol. 18, pp. 194-211, 1979.

[13]

{FK84} Francez, N., and Kozen, D., Generalized Fair Termination, 11th Annual ACM Symp. on Principles of Programming Languages 1984, pp. 46-53.

Digital Library

[14]

{HA84} Harel, D., A General Result on Infinite Trees and Its Applications, 16th STOC, pp. 418-427, May 84.

Digital Library

[15]

{HS84} Hart, S., and Sharir, M., Probabilistic Temporal Logics for Finite and Bounded Models, 16th STOC, pp. 1-13, 1984.

Digital Library

[16]

{KO83} Kozen, D., Results on the Propositional Mu-calculus, Theoretical Computer Science, pp. 333-354, December 83.

[17]

{LA80} Lamport, L., Sometimes is Sometimes "Not Never" - on the temporal logic of programs, 7th Annual ACM Symp. on Principles of Programming Languages, 1980, pp. 174-185.

Digital Library

[18]

{LPS81} Lehmann. D., Pnueli, A., and Stavi, J., Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, ICALP 1981, LNCS Vol. 115, pp. 264-277.

Digital Library

[19]

{LP84} Lichtenstein, O. and Pnueli, A., Checking that Finite State Concurrent Programs Satisfy their Linear Specification, unpublished manuscript, July 84, (to appear this POPL85.)

Digital Library

[20]

{McN66} McNaughton, R., Testing and Generating Infinite Sequences by a Finite Automaton, Information and Control, Vol. 9, 1966.

[21]

{OJ84} Ojala, Leo, Personal Communication at ICALP84, July 1984.

[22]

{OL82} Owicki, S. S., and Lamport, L., Proving Liveness Properties of Concurrent Programs, ACM Trans. on Programming Languages and Syst., Vol. 4, No. 3, July 1982, pp. 455-495.

Digital Library

[23]

{PN77} Pnueli, A., The Temporal Logic of Programs, 19th annual Symp. on Foundations of Computer Science, 1977.

[24]

{PN83} Pnueli, A., On The Extremely Fair Termination of Probabilistic Algorithms, 15 Annual ACM Symp. on Theory of Computing, 1983, 278-290.

Digital Library

[25]

{PR76} Pratt, V., Semantical Considerations on Floyd-Hoare Logic, 17th FOCS, pp. 109-121, 1976.

[26]

{PR81} Pratt, V., A Decidable Mu-Calculus, 22nd FOCS, pp. 421-427, 1981.

[27]

{QS83} Queille, J. P., and Sifakis, J., Fairness and Related Properties in Transition Systems, Acta Informatica, vol. 19, pp. 195-220, 1983.

Digital Library

[28]

{RA69} Rabin, M., Decidability of Second order Theories and Automata on Infinite Trees, Trans. Amer. Math. Society, Vol. 141, pp. 1-35, 1969.

[29]

{RA70} Rabin, M., Automata on Infinite Trees and the Synthesis Problem, Hebrew Univ., Tech. Report no. 37, 1970.

[30]

{SC82} Sistla, A. P., and Clarke, E. M., The Complexity of Propositional Temporal Logic, 14 Annual ACM Symp. on Theory of Computing, 1982.

Digital Library

[31]

{ST81} Streett, R., Propositional Dynamic Logic of Looping and Converse (PhD Thesis), MIT Lab for Computer Science, TR-263, 1981. (a short version appears in STOC81)

[32]

{SE84} Streett, R., and Emerson, E. A., The Propositional Mu-Calculus is Elementary, ICALP84, pp. 465-472, July 84.

Digital Library

[33]

{VW84} Vardi, M. and Wolper, P., Automata Theoretic Techniques for Modal Logics of Programs, pp. 446-455, STOC84.

Digital Library

Cited By

Almagor SYizhaq O(2024)Jumping Automata over Infinite WordsTheory of Computing Systems10.1007/s00224-024-10192-wOnline publication date: 10-Sep-2024
https://doi.org/10.1007/s00224-024-10192-w
Kudalkar VHashemi NMukhopadhyay SMallick SBudnik CNagaraja PDeshmukh J(2024)Sampling-Based and Gradient-Based Efficient Scenario GenerationRuntime Verification10.1007/978-3-031-74234-7_5(70-88)Online publication date: 12-Oct-2024
https://doi.org/10.1007/978-3-031-74234-7_5
Almagor SYizhaq O(2023)Jumping Automata over Infinite WordsDevelopments in Language Theory10.1007/978-3-031-33264-7_2(9-22)Online publication date: 19-May-2023
https://doi.org/10.1007/978-3-031-33264-7_2
Show More Cited By

Index Terms

Modalities for model checking (extended abstract): branching time strikes back

Recommendations

Abstract Model Checking of tccp programs

The Timed Concurrent Constraint programming language (tccp) introduces time aspects into the Concurrent Constraint paradigm. This makes tccp especially appropriate to analyze by model checking timing properties of concurrent systems. However, even if ...
Model Checking Abstract State Machines with Answer Set Programming
This is a SPECIAL ISSUE ON ASM'05

The quality of a computer system can be enhanced by modelling its design and verifying the correctness of the design before implementation is done. Abstract State Machines (ASMs) provide a mathematical framework for system modelling, while Model ...
Counter-example generation in symbolic abstract model-checking

The boundaries of model-checking have been extended through the use of abstraction. These techniques are conservative, in the following sense: when the verification succeeds, the verified property is guaranteed to hold; but when it fails, it may result ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

January 1985

340 pages

ISBN:0897911474

DOI:10.1145/318593

Chairmen:
Mary S. Van Deusen
IBM Watson Research
,
Zvi Galil
Columbia University, New York, NY
,
Brian K. Reid
Stanford Univ., Stanford, CA

Copyright © 1985 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1985

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 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

112
Total Citations
View Citations
866
Total Downloads

Downloads (Last 12 months)143
Downloads (Last 6 weeks)15

Reflects downloads up to 10 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Almagor SYizhaq O(2024)Jumping Automata over Infinite WordsTheory of Computing Systems10.1007/s00224-024-10192-wOnline publication date: 10-Sep-2024
https://doi.org/10.1007/s00224-024-10192-w
Kudalkar VHashemi NMukhopadhyay SMallick SBudnik CNagaraja PDeshmukh J(2024)Sampling-Based and Gradient-Based Efficient Scenario GenerationRuntime Verification10.1007/978-3-031-74234-7_5(70-88)Online publication date: 12-Oct-2024
https://doi.org/10.1007/978-3-031-74234-7_5
Almagor SYizhaq O(2023)Jumping Automata over Infinite WordsDevelopments in Language Theory10.1007/978-3-031-33264-7_2(9-22)Online publication date: 19-May-2023
https://doi.org/10.1007/978-3-031-33264-7_2
Casares ADuret-Lutz AMeyer KRenkin FSickert S(2022)Practical Applications of the Alternating Cycle DecompositionTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-99527-0_6(99-117)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1007/978-3-030-99527-0_6
Casagrande AGentilini RPiazza CPolicriti A(2022)Hybrid Automata in Systems BiologySystems Biology Modelling and Analysis10.1002/9781119716600.ch8(305-338)Online publication date: 18-Nov-2022
https://doi.org/10.1002/9781119716600.ch8
McCabe-Dansted JDixon CFrench TReynolds M(2019)Sublogics of a branching time logic of robustnessInformation and Computation10.1016/j.ic.2019.02.003Online publication date: Mar-2019
https://doi.org/10.1016/j.ic.2019.02.003
Bloemen VDuret-Lutz APol J(2019)Model checking with generalized Rabin and Fin-less automataInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-019-00508-421:3(307-324)Online publication date: 1-Jun-2019
https://dl.acm.org/doi/10.1007/s10009-019-00508-4
Li YTurrini AChen YZhang L(2019)Learning Büchi Automata and Its ApplicationsEngineering Trustworthy Software Systems10.1007/978-3-030-17601-3_2(38-98)Online publication date: 14-Apr-2019
https://doi.org/10.1007/978-3-030-17601-3_2
Belardinelli FLomuscio AMurano ARubin S(2018)Alternating-time temporal logic on finite tracesProceedings of the 27th International Joint Conference on Artificial Intelligence10.5555/3304415.3304428(77-83)Online publication date: 13-Jul-2018
https://dl.acm.org/doi/10.5555/3304415.3304428
Bozzelli LMolinari AMontanari APeron ASala P(2018)Interval vs. Point Temporal Logic Model CheckingACM Transactions on Computational Logic10.1145/328102820:1(1-31)Online publication date: 20-Dec-2018
https://dl.acm.org/doi/10.1145/3281028
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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