Skip to main content
SpringerLink
Log in
SpringerLink
Log in

An effective tableau system for the linear time μ-calculus

  • Session 2: Fairness, Domination, and the μ-Calculus
  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 1996)

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

Included in the following conference series:

Abstract

We present a tableau system for the model checking problem of the linear time μ-calculus. It improves the system of Stirling and Walker by simplifying the success condition for a tableau. In our system success for a leaf is determined by the path leading to it, whereas Stirling and Walker's method requires the examination of a potentially infinite number of paths extending over the whole tableau.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Fitting, Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983).

    Google Scholar 

  2. G.E. Hughes and M.J. Creswell, An Introduction to Modal Logic, (Methuen and Co., 1968)

    Google Scholar 

  3. R. Kaivola, A simple decision method for the linear time mu-calculus, Proc. Int. Workshop on Structures in Concurrency Theory (J. Desel, ed.) (1995)

    Google Scholar 

  4. A. Mader, Tableau recycling, Proc. CAV '92, LNCS 663 (1992).

    Google Scholar 

  5. A. Mader, Modal μ-calculus, model checking and Gauß elimination, Proc. TACAS'95, to appear in LNCS. (1995)

    Google Scholar 

  6. C. P. Stirling, Modal logics for communicating systems. Theoret. Comput. Sci. 49 311–347 (1987).

    Article  Google Scholar 

  7. C. Stirling and D. Walker, CCS, liveness, and local model checking in the linear time mu-calculus, Proc. First International Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407 166–178. (1990).

    Google Scholar 

  8. C. Stirling and D. Walker, Local model checking in the modal mucalculus, Theor. Comput. Sci. 89, 161–177. (1991).

    Article  Google Scholar 

  9. M. Vardi, A temporal fixpoint calculus, Proc. 15th PoPL, 250–259. (1988)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LFCS, University of Edinburgh, King's Buildings, EH9 3JZ, Edinburgh, UK

    Julian Bradfield

  2. Institut für Informatik, Technische Universität München, Arcisstr. 21, 80333, München, Germany

    Javier Esparza & Angelika Mader

Authors
  1. Julian Bradfield
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Javier Esparza
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Angelika Mader
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Friedhelm Meyer Burkhard Monien

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bradfield, J., Esparza, J., Mader, A. (1996). An effective tableau system for the linear time μ-calculus. In: Meyer, F., Monien, B. (eds) Automata, Languages and Programming. ICALP 1996. Lecture Notes in Computer Science, vol 1099. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61440-0_120

Download citation

  • DOI: https://doi.org/10.1007/3-540-61440-0_120

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61440-1

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation