Article

Free access

Avoiding the state explosion problem in temporal logic model checking

Authors:

E. M. Clarke,

O. GrumbergAuthors Info & Claims

PODC '87: Proceedings of the sixth annual ACM Symposium on Principles of distributed computing

Pages 294 - 303

https://doi.org/10.1145/41840.41865

Published: 01 December 1987 Publication History

PDF eReader

References

[1]

B. Alpem and F. Schneider. Verifying Temporal Properties without using Temporal Logic. Tcch. Rept. 85-723, Cornell University Computer Science Department, December. 1985.

Google Scholar

[2]

K. Apt and D. Kozen. "Limits for Automatic Verification of Finite- State Concurrent Systems". Inf. Process. LelL 22, 6 (1986), 307-309.

Digital Library

Google Scholar

[3]

M.C. Browne. An Improved Algorithm for the Automatic Verification of Finite State Systems using Temporal Logic. Proceedings of the 1986 Conference on Logic in Computer Science., Cambridge, Massachusetts, June, 1986, pp, 260-267.

Google Scholar

[4]

M. Browne, E. Clarke, D. Dill, B. Mishra. "Automatic Verification of Sequential Circuits using Temporal Logic". IEEE Transaclions on Computers C-35,12 (December 1986).

Digital Library

Google Scholar

[5]

M. C. Browne, E. M. Clarke, O. Grumberg. Characterizing Kripke Structures in Temporal Logic. Unpublished manuscript, submitted for publication.

Google Scholar

[6]

E.M. Clarke, E.A. Emerson. Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. Proc. of the Workshop on Logic of Programs, Yorktown Heights, NY, 1981.

Digital Library

Google Scholar

[7]

E.M. Clarke, E.A. Emerson, A.P. Sistla. "Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications". ACM Transaclions on Programming languages and Systems 8, 2 (1956), 244-263.

Digital Library

Google Scholar

[8]

E. M. Clarke. O. Grumberg, M. C. Browne. Reasoning about Networks with many identical finite-state processes. Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing., August, 1986. pp. 240-248.

Digital Library

Google Scholar

[9]

David I. Dill and Edmund M. Clarke. "Automatic Verification of Asynchronous Circuits using Temporal Logic". IEE Proceedings 133. pt. E, 5 (September 1986).

Google Scholar

[10]

E.A. Emerson and E.M. Clarke. Characterizing Properties of Parallel Programs as Fixpoints. Proc. of the Seventh International Colloquium on Automata, Languages and Programming, 1981.

Digital Library

Google Scholar

[11]

E.A. Emerson, J.Y. Halpem, ""Sometimes" and "Not Never" Revisited: On Branching versus Linear Time", Proc. 10th ACM Syrup, on Principles of Programming Languages, 1983.

Digital Library

Google Scholar

[12]

E.A. Emerson, Chin Laung Lei. "Modalities for Model Checking: Branching Time Strikes Back". Twelfth Symposium on Principles of Programming Langi~ages, New Orlem~ La. (January 1985).

Digital Library

Google Scholar

[13]

R.M. Karp and R. E. Miller. "Parallel Program Schemata", JCSS, 3 (1969), 147-195.

Digital Library

Google Scholar

[14]

L. Lamport. What Good is Temporal Logic? Proceedings of the International Federation for Information Processing, 1983, pp. 657-668.

Google Scholar

[15]

O. Lichtenstein and A. Pnueli. Checking that Finite State Concurrent Programs Satisfy Their Linear Specification. Conference Record of the Twelth Annual ACM Symposium on Principles of Programming Languages, New Orleans, La., January, 1985.

Digital Library

Google Scholar

[16]

R. Milner. Lecture Notes in Computer Scienc~ Volume 92:A Calculus of Communicatin& Systemx Springer-Verlag, 1979.

Digital Library

Google Scholar

[17]

B. Mishta, E.M. Clarke. "Hierarchical Verification of Asynchronous Circuits using Temporal Logic". Theoretical Computer Science 38 (1985), 269-29L

Crossref

Google Scholar

[18]

C. A, Petri. Fundamentals of a theory of Asynchronous Information Flow. Proceedings of the IFIP Congress 62, Munich, 1962, pp. 386-390.

Google Scholar

[19]

J.P. Quieile, J. Sifakis. "Specification and Verification of Concurrent Systems in CESAR". Proc. of the Filth International Symposium in Programming, 1981.

Google Scholar

[20]

A.P. Sisfla, E.M. Clarke. "Complexity of Propositional Temporal Logics". Journal of the Association for Computing Machinery 32, 3 (J uly 1986), 733-749.

Digital Library

Google Scholar

[21]

P. Sistla and S. German. Reasoning with Many Processes. GTE Laboratories Inc., Waltham, Massachusetts.

Google Scholar

[22]

M. Vardi and P. Wolper. An Automata-Theoretic Approach to Automatic Program Verification. Proceedings of the Conference on Logic in Computer Science, Bogoa, Mass., June, 1986.

Google Scholar

Cited By

View all

Heizmann MKlumpp DNitzke LSchüssele F(2024)Petrification: Software Model Checking for Programs with Dynamic Thread ManagementVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_1(3-25)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_1
Goel ASakallah K(2022)Regularity and quantification: a new approach to verify distributed protocolsInnovations in Systems and Software Engineering10.1007/s11334-022-00460-819:4(359-377)Online publication date: 29-Sep-2022
https://doi.org/10.1007/s11334-022-00460-8
Lowe G(2022)Parameterized verification of systems with component identities, using view abstractionInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00648-024:2(287-324)Online publication date: 26-Feb-2022
https://doi.org/10.1007/s10009-022-00648-0
Show More Cited By

Index Terms

Avoiding the state explosion problem in temporal logic model checking

Recommendations

Methods to Tackle State Explosion Problem in Model Checking
IITA '09: Proceedings of the 2009 Third International Symposium on Intelligent Information Technology Application - Volume 02

Model checking is an automatic verification technique for finite state concurrent systems. In this approach to verification, temporal logic specifications are checked by an exhaustive search of the state space of the concurrent system. The size of the ...
Methods to tackle state explosion problem in model checking
IITA'09: Proceedings of the 3rd international conference on Intelligent information technology application

Model checking is an automatic verification technique for finite state concurrent systems. In this approach to verification, temporal logic specifications are checked by an exhaustive search of the state space of the concurrent system. The size of the ...
Model Checking --- My 27-Year Quest to Overcome the State Explosion Problem
LPAR '08: Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning

Model Checking is an automatic verification technique for state-transition systems that are finite-state or that have finite-state abstractions. In the early 1980's in a series of joint papers with my graduate students E.A. Emerson and A.P. Sistla, we ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PODC '87: Proceedings of the sixth annual ACM Symposium on Principles of distributed computing

December 1987

304 pages

ISBN:089791239X

DOI:10.1145/41840

Editor:
Fred B. Schneider

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 December 1987

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PODC87

Sponsor:

PODC87: Sixth Annual ACM Symposium on Principles of Distributed Computing

August 10 - 12, 1987

British Columbia, Vancouver, Canada

Acceptance Rates

Overall Acceptance Rate 740 of 2,477 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

94
Total Citations
View Citations
834
Total Downloads

Downloads (Last 12 months)64
Downloads (Last 6 weeks)9

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Heizmann MKlumpp DNitzke LSchüssele F(2024)Petrification: Software Model Checking for Programs with Dynamic Thread ManagementVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_1(3-25)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_1
Goel ASakallah K(2022)Regularity and quantification: a new approach to verify distributed protocolsInnovations in Systems and Software Engineering10.1007/s11334-022-00460-819:4(359-377)Online publication date: 29-Sep-2022
https://doi.org/10.1007/s11334-022-00460-8
Lowe G(2022)Parameterized verification of systems with component identities, using view abstractionInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00648-024:2(287-324)Online publication date: 26-Feb-2022
https://doi.org/10.1007/s10009-022-00648-0
Malkis A(2021)Reachability in Parallel Programs Is Polynomial in the Number of ThreadsJournal of Parallel and Distributed Computing10.1016/j.jpdc.2021.11.008Online publication date: Dec-2021
https://doi.org/10.1016/j.jpdc.2021.11.008
Pradeep RSunitha NRavi VVerma S(2020)A Framework for Formal Verification of Security Protocols in C++Inventive Communication and Computational Technologies10.1007/978-981-15-0146-3_17(163-175)Online publication date: 30-Jan-2020
https://doi.org/10.1007/978-981-15-0146-3_17
Singh LRajput H(2018)Dependability Analysis of Safety Critical Real-Time Systems by Using Petri NetsIEEE Transactions on Control Systems Technology10.1109/TCST.2017.266914726:2(415-426)Online publication date: Mar-2018
https://doi.org/10.1109/TCST.2017.2669147
Lowe G(2018)View Abstraction for Systems with Component IdentitiesFormal Methods10.1007/978-3-319-95582-7_30(505-522)Online publication date: 12-Jul-2018
https://doi.org/10.1007/978-3-319-95582-7_30
Lyu HSuraj Nandiganahalli JHwang I(2017)Human Automation Interaction Issue Detection Using a Generalized Fuzzy Hidden Markov ModelAIAA Information Systems-AIAA Infotech @ Aerospace10.2514/6.2017-0344Online publication date: 5-Jan-2017
https://doi.org/10.2514/6.2017-0344
Sánchez ASánchez C(2017)Parametrized verification diagramsAnnals of Mathematics and Artificial Intelligence10.1007/s10472-016-9531-980:3-4(249-282)Online publication date: 1-Aug-2017
https://dl.acm.org/doi/10.1007/s10472-016-9531-9
García-Ferreira ILaorden CSantos IGarcia Bringas P(2016)Static analysis: a brief surveyLogic Journal of IGPL10.1093/jigpal/jzw04224:6(871-882)Online publication date: 16-Sep-2016
https://doi.org/10.1093/jigpal/jzw042
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

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

Cited By

Index Terms

Recommendations

Methods to Tackle State Explosion Problem in Model Checking

Methods to tackle state explosion problem in model checking

Model Checking --- My 27-Year Quest to Overcome the State Explosion Problem