Abstract
We propose a new parameter for the complexity of finite directed graphs which measures to what extent the cycles of the graph are intertwined. This measure, called entanglement, is defined by way of a game that is somewhat similar in spirit to the robber and cops games used to describe tree width, directed tree width, and hypertree width. Nevertheless, on many classes of graphs, there are significant differences between entanglement and the various incarnations of tree width.
Entanglement is intimately connected to the computational and descriptive complexity of the modal μ-calculus. On the one hand, the number of fixed point variables needed to describe a finite graph up to bisimulation is captured by its entanglement. This plays a crucial role in the proof that the variable hierarchy of the μ-calculus is strict.
In addition to this, we prove that parity games of bounded entanglement can be solved in polynomial time. Specifically, we establish that the complexity of solving a parity game can be parametrised in terms of the minimal entanglement of a subgame induced by a winning strategy.
This research has been partially supported by the European Community Research Training Network “Games and Automata for Synthesis and Validation” (games)
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Balcazar, J.L., Diaz, J., Gabarro, J.: Structural complexity 2. Springer, Heidelberg (1988)
Berwanger, D.: Games and Logical Expressiveness, Ph. D. Thesis, RWTH Aachen (2005)
Berwanger, D., Grädel, E., Lenzi, G.: On the variable hierarchy of the modal mu-calculus. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 352–366. Springer, Heidelberg (2002)
Berwanger, D., Lenzi, G.: The variable hierarchy of the μ-calculus is strict. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 97–109. Springer, Heidelberg (2005)
Emerson, A., Jutla, C.: Tree automata, mu-calculus and determinacy. In: Proc. 32nd IEEE Symp. on Foundations of Computer Science, pp. 368–377 (1991)
Johnson, T., Robertson, N., Seymour, P.D., Thomas, R.: Directed treewidth. J. Comb. Theory Ser. B 82, 138–154 (2001)
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)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Obdrzalek, 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)
Seymour, P.D., Thomas, R.: Graph searching and a min-max theorem for tree-width. J. Comb. Theory Ser. B 58, 22–33 (1993)
Stirling, C.: Bisimulation, modal logic and model checking games. Logic Journal of the IGPL 7, 103–124 (1999)
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
Berwanger, D., Grädel, E. (2005). Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games. In: Baader, F., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3452. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32275-7_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-32275-7_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25236-8
Online ISBN: 978-3-540-32275-7
eBook Packages: Computer ScienceComputer Science (R0)