Skip to main content
SpringerLink
Log in

Fixpoint Logics on Hierarchical Structures

  • Conference paper
FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005)

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

Abstract

Hierarchical graph definitions allow a modular description of graphs using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions allow to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems. In this paper, the model-checking problem for the modal μ-calculus and (monadic) least fixpoint logic on hierarchically defined graphs is investigated. In order to analyze the modal μ-calculus, parity games on hierarchically defined graphs are studied.

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst. 23(3), 273–303 (2001)

    Article  Google Scholar 

  2. Dziembowski, S.: Bounded-variable fixpoint queries are PSPACE-complete. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 89–105. Springer, Heidelberg (1997)

    Google Scholar 

  3. Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy (extended abstract). In: Proc. FOCS 1991, pp. 132–142. IEEE Computer Society Press, Los Alamitos (1991)

    Google Scholar 

  4. Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model checking for the μ-calculus and its fragments. Theor. Comput. Sci. 258(1-2), 491–522 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  5. Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In: Proc. LICS 1986, pp. 267–278. IEEE Computer Society Press, Los Alamitos (1986)

    Google Scholar 

  6. Engelfriet, J.: Context-free graph grammars. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages. Beyond Words, vol. 3, pp. 125–213. Springer, Heidelberg (1997)

    Google Scholar 

  7. Göller, S., Lohrey, M.: Fixpoint logics on hierarchical structures. Tech. Rep. 2005/3, University of Stuttgart, Germany (2005), ftp.informatik.uni-stuttgart.de/pub/library/ncstrl.ustuttgart fi/TR-2005-04/

    Google Scholar 

  8. Grädel, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)

    Book  MATH  Google Scholar 

  9. Immerman, N.: Relational queries computable in polynomial time. Inf. Control 68(1-3), 86–104 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  10. Jurdziński, M.: Deciding the winner in parity games is in UP and co-UP. Inf. Process. Lett. 68(3), 119–124 (1998)

    Article  Google Scholar 

  11. Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  12. Lengauer, T.: Hierarchical planarity testing algorithms. J. Assoc. Comput. Mach. 36(3), 474–509 (1989)

    MATH  MathSciNet  Google Scholar 

  13. Lengauer, T., Wagner, K.W.: The correlation between the complexities of the nonhierarchical and hierarchical versions of graph problems. J. Comput. Syst. Sci. 44, 63–93 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  14. Lengauer, T., Wanke, E.: Efficient solution of connectivity problems on hierarchically defined graphs. SIAM J. Comput. 17(6), 1063–1080 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  15. Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  16. Lohrey, M.: Model-checking hierarchical graphs. Tech. Rep. 2005/1, University of Stuttgart, Germany (2005), ftp.informatik.uni-stuttgart.de/pub/library/ncstrl.ustuttgart fi/TR-2005-1/

    Google Scholar 

  17. Lohrey, M.: Model-checking hierarchical structures. In: Proc. LICS 2005, pp. 168–177. IEEE Computer Society Press, Los Alamitos (2005)

    Google Scholar 

  18. Marathe, M.V., Hunt III, H.B., Stearns, R.E., Radhakrishnan, V.: Approximation algorithms for PSPACE-hard hierarchically and periodically specified problems. SIAM J. Comput. 27(5), 1237–1261 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  19. Obdržálek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 80–92. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  20. Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)

    MATH  Google Scholar 

  21. Vardi, M.Y.: The complexity of relational query languages (extended abstract). In: Andersson, S.I. (ed.) Summer University of Southern Stockholm 1993. 137–146, vol. 888, pp. 137–146. Springer, Heidelberg (1995)

    Google Scholar 

  22. Vardi, M.Y.: On the complexity of bounded-variable queries. In: Proc. PODS 1995, pp. 266–276. ACM Press, New York (1995)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FMI, Universität Stuttgart, Germany

    Stefan Göller & Markus Lohrey

Authors
  1. Stefan Göller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Markus Lohrey
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. National Institute of Advanced Studies, Indian Institute of Science Campus, 560012, Bangalore, India

    Sundar Sarukkai

  2. Department of Comp. Sc. & Engg., Indian Institute of Technology Delhi, 110016, New Delhi, India

    Sandeep Sen

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Göller, S., Lohrey, M. (2005). Fixpoint Logics on Hierarchical Structures. In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_39

Download citation

  • DOI: https://doi.org/10.1007/11590156_39

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation