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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst. 23(3), 273–303 (2001)
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)
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)
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)
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)
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)
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/
Grädel, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Immerman, N.: Relational queries computable in polynomial time. Inf. Control 68(1-3), 86–104 (1986)
Jurdziński, M.: Deciding the winner in parity games is in UP and co-UP. Inf. Process. Lett. 68(3), 119–124 (1998)
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)
Lengauer, T.: Hierarchical planarity testing algorithms. J. Assoc. Comput. Mach. 36(3), 474–509 (1989)
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)
Lengauer, T., Wanke, E.: Efficient solution of connectivity problems on hierarchically defined graphs. SIAM J. Comput. 17(6), 1063–1080 (1988)
Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004)
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/
Lohrey, M.: Model-checking hierarchical structures. In: Proc. LICS 2005, pp. 168–177. IEEE Computer Society Press, Los Alamitos (2005)
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)
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)
Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)
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)
Vardi, M.Y.: On the complexity of bounded-variable queries. In: Proc. PODS 1995, pp. 266–276. ACM Press, New York (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)