Skip to main content
SpringerLink
Log in

Model checking and efficient automation of temporal reasoning

  • Invited Paper
  • Conference paper
  • First Online:
CONCUR '95: Concurrency Theory (CONCUR 1995)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 962))

Included in the following conference series:

  • 137 Accesses

This work was supported in part by NSF grant CCR-9415496 and by SRC contract 94-DP-388.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

References

  1. Clarke, E. M., and Emerson, E. A., Design and Verification of Synchronization Skeletons using Branching Time Temporal Logic, Logics of Programs Workshop 1981, Springer LNCS no. 131.

    Google Scholar 

  2. Clarke, E. M., Filkorn, T., Jha, S. Exploiting Symmetry in Temporal Logic Model Checking, 5th International Conference on Computer Aided Verification, Crete, Greece, June 1993; journal version to appear in Formal Methods in System Design.

    Google Scholar 

  3. Emerson, E. A., Evangelist, M., and Srinivasan, J., On the Limits of Efficient Temporal Satisfiability, 5th IEEE Symp. on Logic in Computer Science (LICS), Philadelphia, pp. 464–475, 1990.

    Google Scholar 

  4. Emerson, E. A., Sadler, T. H., and Srinivasan, J., Efficient Temporal Satisfiability, Journal of Logic and Computation, vol. 2, no. 2, pp. 173–210, 1992.

    Google Scholar 

  5. Emerson, E. A., and Sistla, A. P., Symmetry and Model Checking, 5th International Conference on Computer Aided Verification, Crete, Greece, June 1993; journal version to appear in Formal Methods in System Design.

    Google Scholar 

  6. Emerson, E. A., and Sistla, A. P., Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach, to appear in 7th International Conference on Computer Aided Verification, Liege, Belgium, Springer LNCS, July 1995.

    Google Scholar 

  7. Ip, C-W. N., Dill, D. L., Better Verification through Symmetry, Computer Hardware Description Language Conference, April 1993; journal version to appear in Formal Methods in Systems Design.

    Google Scholar 

  8. Jensen, K., Colored Petri Nets: Basic Concepts, Analysis Methods, and Practical Use, vol. 2: Analysis Methods, EATCS Monographs, Springer-Verlag, 1994.

    Google Scholar 

  9. Kurshan, R. P., Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press, Princeton, New Jersey 1994.

    Google Scholar 

  10. Pnueli, A., The Temporal Logic of Programs, 17th IEEE Symp. on Foundations of Computer Science (FOCS), October, 1977.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Texas at Austin, 78712, Austin, Tx, USA

    E. Allen Emerson

Authors
  1. E. Allen Emerson
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Insup Lee Scott A. Smolka

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Emerson, E.A. (1995). Model checking and efficient automation of temporal reasoning. In: Lee, I., Smolka, S.A. (eds) CONCUR '95: Concurrency Theory. CONCUR 1995. Lecture Notes in Computer Science, vol 962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60218-6_29

Download citation

  • DOI: https://doi.org/10.1007/3-540-60218-6_29

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60218-7

  • Online ISBN: 978-3-540-44738-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation