Skip to main content
SpringerLink
Log in

Axiomatising linear time mu-calculus

  • Session: Linear-Time Logics
  • 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:

Abstract

We present a sound and complete axiomatisation for the linear time mu-calculus νTL, a language extending standard linear time temporal logic with fixpoint operators. The completeness proof is based on a new bi-aconjunctive non-alternating normal form for νTL-formulae.

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. Arnold, A. & Niwiński, D.: Fixed Point Characterisation of Weak Monadic Logic Definable Sets of Trees, in Nivat, M. & Podelski, A. (eds.): Tree Automata and Languages, Elsevier, 1992, pp. 159–188

    Google Scholar 

  2. Banieqbal, B. & Barringer, H.: Temporal Logic with Fixed Points, in Temporal Logic in Specification, LNCS vol. 398, Springer-Verlag, 1989, pp. 62–74

    Google Scholar 

  3. Barringer, H. & Kuiper, R. & Pnueli, A.: A Really Abstract Concurrent Model and its Temporal Logic, in Proc. of the 13th ACM POPL, 1986

    Google Scholar 

  4. Dam, M.: Fixpoints of Büchi automata, in Proceedings of the 12th FST & TCS, LNCS vol. 652, Springer-Verlag, 1992, pp. 39–50

    Google Scholar 

  5. Emerson, E. A.: Temporal and Modal Logic, in van Leeuwen, J. (ed.): Handbook of Theoretical Computer Science, Elsevier/North-Holland, 1990, pp. 997–1072

    Google Scholar 

  6. Emerson, E. A. & Lei, C. L.: Efficient Model-Checking in Fragments of the Propositional Mu-calculus, in Proc. of the First IEEE LICS, 1986, pp. 267–278

    Google Scholar 

  7. Kozen, D.: Results on the Propositional μ-calculus, in Theoretical Computer Science, vol. 27, 1983, pp. 333–354

    Article  Google Scholar 

  8. Lichtenstein, O.: Decidability, Completeness, and Extensions of Linear Time Temporal Logic, PhD thesis, The Weizmann Institute of Science, Rehovot, Israel, 1991

    Google Scholar 

  9. McNaughton, R.: Testing and Generating Infinite Sequences by a Finite Automaton, in Information and Control, vol. 9, 1966, pp. 521–530

    Google Scholar 

  10. Muller, D.E. & Saoudi, A. & Schupp, P.: Alternating Automata, the Weak Monadic Theory of the Tree, and its Complexity, in Proc. of the 13th ICALP, LNCS vol. 226, Springer-Verlag, 1986, pp. 275–283

    Google Scholar 

  11. Niwiński, D.: On Fixed Point Clones, in Proc. of the 13th ICALP, LNCS vol. 226, Springer-Verlag, 1986, pp. 402–409

    Google Scholar 

  12. Siefkes, D.: Büchi's Monadic Second Order Successor Arithmetic, Decidable Theories I, LNM vol. 120, Springer-Verlag, 1970

    Google Scholar 

  13. Stirling, C.: Modal and Temporal Logics, in Abramsky, S. & al. (eds.): Handbook of Logic in Computer Science, Oxford University Press, 1992, pp. 477–563

    Google Scholar 

  14. Stirling, C. & Walker, D.: Local Model Checking in the Modal Mu-calculus, in Theoretical Computer Science, vol. 89, 1991, pp. 161–177

    Article  Google Scholar 

  15. Streett, R. S. & Emerson, E. A.: An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus, in Information and Computation, vol. 81, 1989, pp. 249–264

    Article  Google Scholar 

  16. Thomas, W.: Automata on Infinite Objects, in van Leeuwen, J. (ed.): Handbook of Theoretical Computer Science, vol. 2, North-Holland, 1989, pp. 133–191

    Google Scholar 

  17. Vardi, M. Y.: A Temporal Fixpoint Calculus, in Proceedings of the 15th ACM Symposium on Priciples of Programming Languages, 1988, pp. 250–259

    Google Scholar 

  18. Vardi, M. Y. & Wolper, P.: Reasoning about Infinite Computations, in Information and Computation, vol. 115, 1994, pp. 1–37

    Article  Google Scholar 

  19. Walukiewicz, I.: On Completeness of the μ-calculus, in Proc. of the 8th IEEE LICS, 1993, pp. 136–146

    Google Scholar 

  20. Walukiewicz, I.: Completeness of Kozen's Axiomatisation of the Propositional μ-calculus, to appear in Proc. of the 10th IEEE LICS, 1995

    Google Scholar 

  21. Wolper, P.: Synthesis of Communicating Processes from Temporal Logic Specifications, PhD thesis, Stanford University, 1982

    Google Scholar 

  22. Wolper, P.: Temporal Logic can be More Expressive, in Information and Control, vol 56, 1983, pp. 72–99

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory for Foundations of Computer Science, University of Edinburgh, The King's Buildings, EH9 3JZ, Edinburgh, UK

    Roope Kaivola

Authors
  1. Roope Kaivola
    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

Kaivola, R. (1995). Axiomatising linear time mu-calculus. 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_32

Download citation

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

  • 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