×

Courcelle’s theorem – a game-theoretic approach. (English) Zbl 1235.68103

Summary: Courcelle’s theorem states that every problem definable in monadic second-order logic can be solved in linear time on structures of bounded treewidth, for example, by constructing a tree automaton that recognizes or rejects a tree decomposition of the structure. Existing, optimized software like the MONA tool can be used to build the corresponding tree automata, which for bounded treewidth are of constant size. Unfortunately, the constants involved can become extremely large – every quantifier alternation requires a power set construction for the automaton. Here, the required space can become a problem in practical applications.
In this paper we present a novel, direct approach based on model checking games, which avoids the expensive power set construction. Experiments with an implementation are promising, and we can solve problems on graphs where the automata-theoretic approach fails in practice.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B15 Higher-order logic; type theory (MSC2010)
91A80 Applications of game theory

Software:

MONA; ComputeTW
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Courcelle, B., The monadic second order theory of graphs I: recognisable sets of finite graphs, Inform. Comput., 85, 12-75 (1990) · Zbl 0722.03008
[2] Frick, M.; Grohe, M., The complexity of first-order and monadic second-order logic revisited, Ann. Pure Appl. Logic, 130, 1-3, 3-31 (2004) · Zbl 1062.03032
[3] Arnborg, S.; Lagergren, J.; Seese, D., Easy problems for tree-decomposable graphs, J. Algorithms, 12, 2, 308-340 (1991) · Zbl 0734.68073
[4] Courcelle, B.; Mosbah, M., Monadic second-order evaluations on tree-decomposable graphs, Theoret. Comput. Sci., 109, 1-2, 49-82 (1993) · Zbl 0789.68083
[5] Courcelle, B., Graph rewriting: an algebraic and logic approach, (Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B) (1990), Elsevier), 193-242 · Zbl 0900.68282
[6] Downey, R. G.; Fellows, M. R., Parameterized Complexity (1999), Springer-Verlag · Zbl 0914.68076
[7] Flum, J.; Frick, M.; Grohe, M., Query evaluation via tree-decompositions, J. ACM, 49, 6, 716-752 (2002) · Zbl 1326.68123
[8] Flum, J.; Grohe, M., Parameterized Complexity Theory (2006), Springer-Verlag
[9] M. Weyer, Modifizierte parametrische Komplexitätstheorie, Ph.D. Thesis, Universität Freiburg, 2008.; M. Weyer, Modifizierte parametrische Komplexitätstheorie, Ph.D. Thesis, Universität Freiburg, 2008.
[10] B. Courcelle, J. Engelfriet, Graph Structure and Monadic Second-Order Logic, A Language Theoretic Approach, Cambridge University Press, 2011 (submitted for publication).; B. Courcelle, J. Engelfriet, Graph Structure and Monadic Second-Order Logic, A Language Theoretic Approach, Cambridge University Press, 2011 (submitted for publication). · Zbl 1257.68006
[11] Feferman, S.; Vaught, R., The first order properties of algebraic systems, Fund. Math., 47, 57-103 (1959) · Zbl 0088.24803
[12] Gurevich, Y., Modest theory of short chains. I, J. Symbolic Logic, 44, 4, 481-490 (1979) · Zbl 0464.03013
[13] M. Frick, Easy instances for model checking, Ph.D. Thesis, Universität Freiburg, 2001.; M. Frick, Easy instances for model checking, Ph.D. Thesis, Universität Freiburg, 2001. · Zbl 0977.68058
[14] Makowsky, J. A., Algorithmic uses of the Feferman-Vaught theorem, Ann. Pure Appl. Logic, 126, 1-3, 159-213 (2004) · Zbl 1099.03009
[15] Grohe, M., Logic, graphs, and algorithms, (Flum, J.; Grädel, E.; Wilke, T., Logic and Automata: History and Perspectives (2007), Amsterdam University Press: Amsterdam University Press Amsterdam), 357-422 · Zbl 1244.03053
[16] N. Klarlund, A. Møller, MONA version 1.4 user manual, BRICS, Dept. of Comp. Sc., University of Aarhus, Available from: http://www.brics.dk/mona/; N. Klarlund, A. Møller, MONA version 1.4 user manual, BRICS, Dept. of Comp. Sc., University of Aarhus, Available from: http://www.brics.dk/mona/
[17] Klarlund, N.; Møller, A.; Schwartzbach, M. I., MONA implementation secrets, (Proc. of CIAA00 (2001), Springer-Verlag), 182-194 · Zbl 0989.03500
[18] D. Soguet, Génération automatique d’algorithmes linéaires, Doctoral Dissertation, University Paris-Sud, 2008.; D. Soguet, Génération automatique d’algorithmes linéaires, Doctoral Dissertation, University Paris-Sud, 2008.
[19] Courcelle, B.; Makowsky, J. A.; Rotics, U., Linear time solvable optimization problems on graphs of bounded clique width, Theory Comput. Syst., 33, 125-150 (2000) · Zbl 1009.68102
[20] Courcelle, B., Graph structure and monadic second-order logic: language theoretical aspects, (Proceedings of the 35th International Colloquium on Automata, Languages, and Programming. Proceedings of the 35th International Colloquium on Automata, Languages, and Programming, ICALP. Proceedings of the 35th International Colloquium on Automata, Languages, and Programming. Proceedings of the 35th International Colloquium on Automata, Languages, and Programming, ICALP, Lecture Notes in Computer Science, vol. 5125 (2008), Springer), 1-13 · Zbl 1143.68433
[21] Gottlob, G.; Pichler, R.; Wei, F., Abduction with bounded treewidth: from theoretical tractability to practically efficient computation, (Proc. of 23rd AAAI (2008), AAAI Press), 1541-1546
[22] Gottlob, G.; Pichler, R.; Wei, F., Monadic datalog over finite structures of bounded treewidth, ACM Trans. Comput. Log., 12, 1, 3:1-3:48 (2010) · Zbl 1351.68110
[23] B. Courcelle, I.A. Durand, Verifying monadic second-order graph properties with tree automata, in: C. Rhodes (Ed.), 3rd European Lisp Symposium, Informal Proceedings, 2010, pp. 7-21.; B. Courcelle, I.A. Durand, Verifying monadic second-order graph properties with tree automata, in: C. Rhodes (Ed.), 3rd European Lisp Symposium, Informal Proceedings, 2010, pp. 7-21.
[24] B. Courcelle, I.A. Durand, Tractable constructions of finite automata from monadic second-order formulas, presented at Logical Approaches to Barriers in Computing and Complexity, Greifswald, Germany, 2010.; B. Courcelle, I.A. Durand, Tractable constructions of finite automata from monadic second-order formulas, presented at Logical Approaches to Barriers in Computing and Complexity, Greifswald, Germany, 2010.
[25] Courcelle, B., Special tree-width and the verification of monadic second-order graph properties, (Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science. Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS. Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science. Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, Leibniz International Proceedings in Informatics, LIPIcs, vol. 8 (2010), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl Germany), 13-29 · Zbl 1245.68133
[26] Hintikka, J., Logic, Language-Games and Information: Kantian Themes in the Philosophy of Logic (1973), Clarendon Press · Zbl 0253.02005
[27] Grädel, E., Finite model theory and descriptive complexity, (Finite Model Theory and its Applications (2007), Springer), 125-230
[28] Grädel, E., Back and forth between logics and games, (Apt, K. R.; Grädel, E., Lectures in Game Theory for Computer Scientists (2011), Cambridge University Press), 99-145 · Zbl 1244.03108
[29] Abrahamson, K. A.; Fellows, M. R., Finite automata, bounded treewidth, and well-quasiordering, (Graph Structure Theory. Graph Structure Theory, Contemporary Mathematics, vol. 147 (1993), American Mathematical Society), 539-564 · Zbl 0791.05094
[30] Thatcher, J. W.; Wright, J. B., Generalized finite automata theory with an application to a decision problem of second-order logic, Math. Syst. Theory, 2, 1, 57-81 (1968) · Zbl 0157.02201
[31] Doner, J., Tree acceptors and some of their applications, J. Comput. System Sci., 4, 406-451 (1970) · Zbl 0212.02901
[32] Ganzow, T.; Kaiser, Ł., New algorithm for weak monadic second-order logic on inductive structures, (Proceedings of the 24th International Workshop on Computer Science Logic. Proceedings of the 24th International Workshop on Computer Science Logic, CSL. Proceedings of the 24th International Workshop on Computer Science Logic. Proceedings of the 24th International Workshop on Computer Science Logic, CSL, Lecture Notes in Computer Science, vol. 6247 (2010), Springer), 366-380 · Zbl 1287.68109
[33] Miltersen, P. B.; Radhakrishnan, J.; Wegener, I., On converting CNF to DNF, Theoret. Comput. Sci., 347, 1-2, 325-335 (2005) · Zbl 1080.94018
[34] B. Courcelle, On the model-checking of monadic second-order formulas with edge set quantifications, Discrete Appl. Math. (in press).; B. Courcelle, On the model-checking of monadic second-order formulas with edge set quantifications, Discrete Appl. Math. (in press). · Zbl 1236.05143
[35] McMillan, K. L., A technique of state space search based on unfolding, Form. Methods Syst. Des., 6, 45-65 (1995) · Zbl 0829.68085
[36] Ebbinghaus, H.-D.; Flum, J., Finite Model Theory (1999), Springer
[37] Ganian, R.; Hliněný, P., On parse trees and Myhill-Nerode-type tools for handling graphs of bounded rank-width, Discrete Appl. Math., 158, 7, 851-867 (2010) · Zbl 1231.05096
[38] Robertson, N.; Seymour, P. D., Graph minors. II. Algorithmic aspects of tree-width, J. Algorithms, 7, 309-322 (1986) · Zbl 0611.05017
[39] Diestel, R., Graph Theory (2010), Springer-Verlag: Springer-Verlag Heidelberg · Zbl 1204.05001
[40] Arnborg, S.; Corneil, D. G.; Proskurowski, A., Complexity of finding embeddings in a \(k\)-tree, SIAM J. Algebr. Discrete Methods, 8, 277-284 (1987) · Zbl 0611.05022
[41] Bodlaender, H. L., A linear time algorithm for finding tree-decompositions of small treewidth, SIAM J. Comput., 25, 1305-1317 (1996) · Zbl 0864.68074
[42] Bodlaender, H.; Koster, A. M.C. A., Treewidth computations I. Upper bounds, Inform. Comput., 208, 3, 259-275 (2010) · Zbl 1186.68328
[43] Bodlaender, H. L.; Koster, A. M.C. A., Treewidth computations II. Lower bounds, Inform. Comput., 209, 7, 1103-1119 (2011) · Zbl 1220.68071
[44] Bodlaender, H. L., A tourist guide through treewidth, Acta Cybernet., 11, 1-21 (1993) · Zbl 0804.68101
[45] Bodlaender, H. L., A partial \(k\)-arboretum of graphs with bounded treewidth, Theoret. Comput. Sci., 209, 1-45 (1998) · Zbl 0912.68148
[46] Tarski, A., The semantic conception of truth, Philos. Phenomenolog. Res., 4, 13-47 (1944)
[47] Baier, C.; Katoen, J.-P., (Principles of Model Checking. Principles of Model Checking, Representation and Mind Series (2008), The MIT Press)
[48] Telle, J. A.; Proskurowski, A., Algorithms for vertex partitioning problems on partial \(k\)-trees, SIAM J. Discrete Math., 10, 4, 529-550 (1997) · Zbl 0885.68118
[49] van Rooij, J. M.M.; Bodlaender, H. L.; Rossmanith, P., Dynamic programming on tree decompositions using generalised fast subset convolution, (ESA. ESA, Lecture Notes in Computer Science, vol. 5757 (2009), Springer), 566-577 · Zbl 1256.68157
[50] D. Lokshtanov, D. Marx, S. Saurabh, Known algorithms on graphs on bounded treewidth are probably optimal, in: Proceedings of the 22th ACM-SIAM Symposium on Discrete Algorithms, SODA, 2011, pp. 777-789.; D. Lokshtanov, D. Marx, S. Saurabh, Known algorithms on graphs on bounded treewidth are probably optimal, in: Proceedings of the 22th ACM-SIAM Symposium on Discrete Algorithms, SODA, 2011, pp. 777-789. · Zbl 1373.68242
[51] Alber, J.; Niedermeier, R., Improved tree decomposition based algorithms for domination-like problems, (Proceedings of the 5th Symposium on Latin American Theoretical Informatics. Proceedings of the 5th Symposium on Latin American Theoretical Informatics, LATIN. Proceedings of the 5th Symposium on Latin American Theoretical Informatics. Proceedings of the 5th Symposium on Latin American Theoretical Informatics, LATIN, Lecture Notes in Computer Science, vol. 2286 (2002), Springer: Springer Cancun, Mexico), 613-627 · Zbl 1059.68598
[52] Bodlaender, H. L., Necessary edges in \(k\)-chordalisations of graphs, J. Comb. Optim., 7, 3, 283-290 (2003) · Zbl 1031.05120
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.