Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Verification, Model Checking, and Abstract Interpretation

VMCAI 2005: Verification, Model Checking, and Abstract Interpretation pp 267–281Cite as

Weak Automata for the Linear Time μ-Calculus

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3385))

Abstract

This paper presents translations forth and back between formulas of the linear time μ-calculus and finite automata with a weak parity acceptance condition. This yields a normal form for these formulas, in fact showing that the linear time alternation hierarchy collapses at level 0 and not just at level 1 as known so far. The translation from formulas to automata can be optimised yielding automata whose size is only exponential in the alternation depth of the formula.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: Proc. 13th Annual ACM Symp. on Principles of Programming Languages, pp. 173–183. ACM, New York (1986)

    Google Scholar 

  2. Békić, H.: In: Bekic, H. (ed.) Programming Languages and their Definition. LNCS, vol. 177. Springer, Heidelberg (1984)

    Google Scholar 

  3. Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 193. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  4. Bradfield, J.C.: The modal μ-calculus alternation hierarchy is strict. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 233–246. Springer, Heidelberg (1996)

    Google Scholar 

  5. Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Congress on Logic, Method, and Philosophy of Science, pp. 1–12. Stanford University Press, Stanford (1962)

    Google Scholar 

  6. Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the ACM 28(1), 114–133 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  7. Dziembowski, S., Jurdziński, M., Walukiewicz, I.: How much memory is needed to win infinite games? In: Proc. 12th Symp. on Logic in Computer Science, LICS 1997, Warsaw, Poland, pp. 99–110. IEEE, Los Alamitos (1997)

    Google Scholar 

  8. Emerson, E.A.: Model checking and the μ-calculus. In: Immerman, N., Kolaitis, P.G. (eds.) Descriptive Complexity and Finite Models, ch. 6. DIMACS: Series in Discrete Mathematics and Theoretical Computer Science, vol. 31, AMS (1997)

    Google Scholar 

  9. Emerson, E.A., Jutla, C.S.: Tree automata, μ-calculus and determinacy. In: Proc. 32nd Symp. on Foundations of Computer Science, San Juan, Puerto Rico, pp. 368–377. IEEE, Los Alamitos (1991)

    Google Scholar 

  10. Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional μ-calculus with respect to monadic second order logic. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263–277. Springer, Heidelberg (1996)

    Google Scholar 

  11. Kaivola, R.: Using Automata to Characterise Fixed Point Temporal Logics. PhD thesis, LFCS, Division of Informatics, The University of Edinburgh, Tech. Rep. ECS-LFCS-97-356 (1997)

    Google Scholar 

  12. Kozen, D.: Results on the propositional μ-calculus. TCS 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  13. Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(3), 408–429 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  14. Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM 47(2), 312–360 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  15. Löding, C., Thomas, W.: Alternating automata and logics over infinite words. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 521–535. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  16. Muller, D., Schupp, P.: Alternating automata on infinite objects: determinacy and rabin’s theorem. In: Perrin, D., Nivat, M. (eds.) Automata on Infinite Words. LNCS, vol. 192, pp. 100–107. Springer, Heidelberg (1985)

    Google Scholar 

  17. Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proc. 3rd Symp. on Logic in Computer Science, LICS 1988, Edinburgh, Scotland, pp. 422–427. IEEE, Los Alamitos (1988)

    Google Scholar 

  18. Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. of Amer. Math. Soc. 141, 1–35 (1969)

    MATH  MathSciNet  Google Scholar 

  19. Stirling, C.: Local model checking games. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 1–11. Springer, Heidelberg (1995)

    Google Scholar 

  20. Vardi, M.Y.: A temporal fixpoint calculus. In: Proc. Conf. on Principles of Programming Languages, POPL 1988, pp. 250–259. ACM Press, New York (1988)

    Google Scholar 

  21. Vardi, M.Y.: An Automata-Theoretic Approach to Linear Temporal Logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043. Springer, Heidelberg (1996)

    Google Scholar 

  22. Walukiewicz, I.: Completeness of Kozen’s axiomatization of the propositional μ- calculus. In: Proc. 10th Symp. on Logic in Computer Science, LICS 1995, pp. 14–24. IEEE, Los Alamitos (1995)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, University of Munich, Germany

    Martin Lange

Authors
  1. Martin Lange
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. CNRS, Paris, France

    Radhia Cousot

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lange, M. (2005). Weak Automata for the Linear Time μ-Calculus. In: Cousot, R. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2005. Lecture Notes in Computer Science, vol 3385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30579-8_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30579-8_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-24297-0

  • Online ISBN: 978-3-540-30579-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation