Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Mathematical Foundations of Computer Science

MFCS 2005: Mathematical Foundations of Computer Science 2005 pp 640–651Cite as

The Complexity of Model Checking Higher Order Fixpoint Logic

  • Conference paper

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

Abstract

This paper analyzes the computational complexity of the model checking problem for Higher Order Fixpoint Logic – the modal μ-calculus enriched with a typed λ-calculus. It is hard for every level of the elementary time/space hierarchy and in elementary time/space when restricted to formulas of bounded type order.

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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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. Bar-Hillel, Y., Perles, M., Shamir, E.: On formal properties of simple phrase structure grammars. Zeitschrift für Phonologie, Sprachwissenschaft und Kommunikationsforschung 14, 113–124 (1961)

    MathSciNet  Google Scholar 

  2. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

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

    Google Scholar 

  4. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  6. Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)

    Article  MATH  Google Scholar 

  7. Dawar, A., Grädel, E., Kreutzer, S.: Inflationary fixed points in modal logic. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 277–291. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Emerson, E.A.: Uniform inevitability is tree automaton ineffable. Information Processing Letters 24(2), 77–79 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  9. Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences 30, 1–24 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  10. Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: On branching versus linear time temporal logic. Journal of the ACM 33(1), 151–178 (1986)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  12. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18(2), 194–211 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  13. Harel, D., Pnueli, A., Stavi, J.: Propositional dynamic logic of nonregular programs. Journal of Computer and System Sciences 26(2), 222–243 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  14. Henriksen, J.G., Jensen, J., Joergensen, M., Klarlund, N.: MONA: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89–110. Springer, Heidelberg (1995)

    Google Scholar 

  15. 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 

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

    Article  MATH  MathSciNet  Google Scholar 

  17. Lange, M., Stirling, C.: Model checking fixed point logic with chop. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 250–263. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  18. Müller-Olm, M.: A modal fixpoint logic with chop. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 510–520. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  19. Pnueli, A.: The temporal logic of programs. In: Proc. 18th Symp. on Foundations of Computer Science, FOCS 1977, Providence, RI, USA, oct 1977, pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)

    Google Scholar 

  20. Reinhardt, K.: 13 the complexity of translating logic to finite automata. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 231–238. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  21. Statman, R.: The typed λ-calculus is not elementary recursive. Theoretical Computer Science 9, 73–81 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  22. Stockmeyer, L.: The Computational Complexity of Word Problems. PhD thesis, MIT (1974)

    Google Scholar 

  23. Viswanathan, M., Viswanathan, R.: A higher order modal fixed point logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 512–528. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Martin Lange

  2. IT department, Uppsala University, Sweden

    Rafał Somla

Authors
  1. Martin Lange
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rafał Somla
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Mathematics, Gdansk University, Wita Stwosza 57, 80 952, Gdansk, Poland

    Joanna Jȩdrzejowicz  & Andrzej Szepietowski  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lange, M., Somla, R. (2005). The Complexity of Model Checking Higher Order Fixpoint Logic. In: Jȩdrzejowicz, J., Szepietowski, A. (eds) Mathematical Foundations of Computer Science 2005. MFCS 2005. Lecture Notes in Computer Science, vol 3618. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11549345_55

Download citation

  • DOI: https://doi.org/10.1007/11549345_55

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28702-5

  • Online ISBN: 978-3-540-31867-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation