Implementation of Propositional Temporal Logics Using BDDs | SpringerLink
Skip to main content
Springer Nature Link
Log in

Implementation of Propositional Temporal Logics Using BDDs

  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1998)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1397))

Abstract

This tutorial intends to convey the step-by-step process by which computer programs for model checking and satisfiability testing for temporal logics may be derived from the theory. The idea is to demonstrate that it is very well possible to implement such a program in an efficient way without sacrificing a correct-by-construction approach. The tutorial will be fully self-contained, only a general knowledge of programming and propositional logic is assumed.

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

Similar content being viewed by others

References

  1. Z. Manna, A. Pnueli, “Verification of concurrent programs: the temporal framework,” The Correctness Problem in Computer Science, eds. Robert S. Boyer, J. Strother Moore, International Lecture Series in Computer Science, Academic Press, New York, 1981.

    Google Scholar 

  2. J.R. Burch, E.M. Clarke, K.L. McMillan, “Symbolic Model Checking: 1020 States and Beyond,” International Workshop on Formal Methods in VLSI Design, 1991.

    Google Scholar 

  3. E. Clarke, O. Grumberg, K. Hamaguchi, “Another Look at LTL Model Checking,” Proceeding 6-th Int. Conf. on Computer Aided Verification, Springer-Verlag, LNCS 818, ed. David L. Dill, pp. 415–427.

    Google Scholar 

  4. Geert L.J.M. Janssen, “Hardware Verification using Temporal Logic: A Practical View,” Formal VLSI Correctness Verification, VLSI Design Methods-II, Elsevier Science Publishers B.V. (North-Holland), ed. L.J.M. Claesen, IFIP, 1990, pp. 159–168.

    Google Scholar 

  5. Randal E. Bryant, “Graph-Based Algorithms for Boolean Function Manipulation,” IEEE Transactions on Computers, Vol. C-35, Nr. 8, August 1986.

    Google Scholar 

  6. Karl S. Brace, Richard L. Rudell, Randal E. Bryant, “Efficient Implementation of a BDD Package,” Proceedings Design Automation Conference, June 1990.

    Google Scholar 

  7. Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.

    Google Scholar 

  8. E.A. Emerson, “Chapter 16: Temporal and Modal Logic,” Handbook of Theoretical Computer Science, B: Formal Models and Semantics, ed. Jan van Leeuwen, Elsevier Science Publishers B.V., 1990, pp. 996–1072.

    Google Scholar 

  9. Rance Cleaveland, “Tableau-Based Model Checking in the Propositional Mu-Calculus,” Acta Informatica, No. 27, 1990, pp. 725–747.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Electrical Engineering, Eindhoven University of Technology, Room EH 9.26, P.O. Box 513, 5600 MB, Eindhoven

    G. L. J. M. Janssen

Authors
  1. G. L. J. M. Janssen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Philosophy, Tilburg University, P.O. Box 90153, 5000 LE, Tilburg, The Netherlands

    Harrie de Swart

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Janssen, G.L.J.M. (1998). Implementation of Propositional Temporal Logics Using BDDs. In: de Swart, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1998. Lecture Notes in Computer Science(), vol 1397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-69778-0_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-69778-0_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64406-4

  • Online ISBN: 978-3-540-69778-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation