Skip to main content
SpringerLink
Log in

Space-Efficient Fragments of Higher-Order Fixpoint Logic

  • Conference paper
  • First Online:
Reachability Problems (RP 2017)

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

Included in the following conference series:

Abstract

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed \(\lambda \)-calculus into the modal \(\mu \)-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most \(k > 0\). In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in \((k-1)\)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.

F. Bruse—This work was supported by a fellowship within the FITweltweit programme of the German Academic Exchange Service (DAAD).

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

Access this chapter

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 EPUB and 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

Institutional subscriptions

References

  1. Andersen, H.R.: A polyadic modal \(\mu \)-calculus. Technical Report ID-TR: 1994–195, Dept. of Computer Science, Technical University of Denmark, Copenhagen (1994)

    Google Scholar 

  2. Axelsson, R., Lange, M.: Model checking the first-order fragment of higher-order fixpoint logic. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 62–76. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75560-9_7

    Chapter  Google Scholar 

  3. Axelsson, R., Lange, M., Somla, R.: The complexity of model checking higher-order fixpoint logic. Logical Meth. Comput. Sci. 3, 1–33 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  4. Emerson, E.A.: Uniform inevitability is tree automaton ineffable. Inf. Process. Lett. 24(2), 77–79 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  5. Harel, D., Pnueli, A., Stavi, J.: Propositional dynamic logic of nonregular programs. J. Comput. Syst. Sci. 26(2), 222–243 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  6. Hartmanis, J., Stearns, R.E.: On the computational complexity of algorithms. Trans. AMS 117, 285–306 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  7. Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional \(\mu \)-calculus with respect to monadic second order logic. In: CONCUR, pp. 263–277 (1996)

    Google Scholar 

  8. Jones, N.D.: The expressive power of higher-order types or, life without CONS. J. Funct. Progm. 11(1), 5–94 (2001)

    MathSciNet  MATH  Google Scholar 

  9. Kozen, D.: Results on the propositional \(\mu \)-calculus. TCS 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  10. Lange, M.: Model checking propositional dynamic logic with all extras. J. Appl. Logic 4(1), 39–49 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  11. Lange, M.: Temporal logics beyond regularity. Habilitation thesis, University of Munich, BRICS research report RS-07-13 (2007)

    Google Scholar 

  12. Lange, M., Lozes, E.: Capturing bisimulation-invariant complexity classes with higher-order modal fixpoint logic. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 90–103. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44602-7_8

    Google Scholar 

  13. Lange, M., Somla, R.: Propositional dynamic logic of context-free programs and fixpoint logic with chop. Inf. Process. Lett. 100(2), 72–75 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  14. Otto, M.: Bisimulation-invariant PTIME and higher-dimensional \(\mu \)-calculus. Theor. Comput. Sci. 224(1–2), 237–265 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  15. Savitch, W.J.: Relationships between nondeterministic and deterministic tape complexities. J. Comput. Syst. Sci. 4, 177–192 (1970)

    Article  MathSciNet  MATH  Google Scholar 

  16. Stearns, R.E., Hartmanis, J., Lewis II, P.M.: Hierarchies of memory limited computations. In: Proceedings of the 6th Annual Symposium on Switching Circuit Theory and Logical Design, pp. 179–190. IEEE (1965)

    Google Scholar 

  17. van Emde Boas, P.: The convenience of tilings. In: Sorbi, A. (ed.) Complexity, Logic, and Recursion Theory, vol. 187 of Lecture Notes in Pure and Applied Mathematics, pp. 331–363. Marcel Dekker Inc (1997)

    Google Scholar 

  18. 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). doi:10.1007/978-3-540-28644-8_33

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Kassel, Kassel, Germany

    Florian Bruse & Martin Lange

  2. LSV, ENS Paris-Saclay, CNRS, Cachan, France

    Florian Bruse & Etienne Lozes

Authors
  1. Florian Bruse
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Lange
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Etienne Lozes
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Florian Bruse .

Editor information

Editors and Affiliations

  1. Royal Holloway University of London, London, United Kingdom

    Matthew Hague

  2. University of Liverpool, Liverpool, United Kingdom

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Bruse, F., Lange, M., Lozes, E. (2017). Space-Efficient Fragments of Higher-Order Fixpoint Logic. In: Hague, M., Potapov, I. (eds) Reachability Problems. RP 2017. Lecture Notes in Computer Science(), vol 10506. Springer, Cham. https://doi.org/10.1007/978-3-319-67089-8_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67089-8_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67088-1

  • Online ISBN: 978-3-319-67089-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation