Skip to main content
SpringerLink
Log in

Courcelle’s Theorem

  • Chapter
Fundamentals of Parameterized Complexity

Part of the book series: Texts in Computer Science ((TCS))

  • 3555 Accesses

Abstract

We examine monadic second-order logic MS2 for graphs. We give a “Myhill–Nerode” proof of Courcelle’s Theorem: that MS2 model checking, parameterized by the treewidth of the input graph, and the size of the MS2 formula, is linear time fixed-parameter tractable. Seese’s Theorem, and MS1 logic are also surveyed.

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 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 139.99
Price excludes VAT (USA)
  • Durable hardcover 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

Notes

  1. 1.

    The reader needs to be aware that our universe has now changed from the universe of (isomorphism types of) graphs to the universe of (isomorphism types of) σ-partially equipped graphs. These objects will thus be tuples consisting of graphs together with distinguished parts. Isomorphism here consists of the obvious maps that must send graphs to graphs as well as preserving the relevant distinguished sets of edges, vertices, etc. One can think of these distinguished sets of objects as colored portions of the graphs. It is important that the reader understand that many of the statements to follow talk about differing universes of not just t-boundaried graphs but σ-partially equipped t-boundaried graphs for various σ.

  2. 2.

    Note that this is in the large universe.

  3. 3.

    There is also “on the fly” work of Courcelle and Durant [177] which use what they call fly-automata, and seem to be implementable.

  4. 4.

    Recall that a graph G is said to be a minor of a graph H iff G is represented in H by disjoint paths; that is, there is an injection f:V(G)↦V(H) such that for all xy∈E(G), there is a path p(xy) from f(x) to f(y) in H such that if xy≠x′y′, then p(xy) is disjoint from p(x′y′). We write G≤minor H. We refer the reader to Definition 17.1.7. We will discuss this concept in some detail in the next chapter.

  5. 5.

    The proof of this result is beyond the scope of this book, but a related “excluded minor” theorem is treated in Sect. 18.2.

  6. 6.

    Kabanets [426] is an extended abstract and the full proof only appears in his masters thesis, Kabanets [425].

References

  1. K. Abrahamson, M. Fellows, Cutset regularity beats well-quasi-ordering for bounded treewidth, Preprint (1989)

    Google Scholar 

  2. K. Abrahamson, M. Fellows, Finite automata, bounded treewidth, and well-quasiordering, in Proceedings of the AMS Summer Workshop on Graph Minors, Graph Structure Theory, ed. by N. Robertson, P. Seymour. Contemporary Mathematics, vol. 147 (Am. Math. Soc., Providence, 1993), pp. 539–564

    Google Scholar 

  3. S. Arnborg, Efficient algorithms for combinatorial problems on graphs with bounded decomposability—a survey. BIT Numer. Math. 25(1), 2–23 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  4. S. Arnborg, J. Lagergren, D. Seese, Easy problems for tree-decomposable graphs. J. Algorithms 12(2), 308–340 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  5. H. Bodlaender, M. Fellows, M. Hallett, Beyond NP-completeness for problems of bounded width (extended abstract): hardness for the w hierarchy, in Proceedings of 26th ACM Symposium on Theory of Computing (STOC ’94), Montréal, Québec, Canada, May 23–May 25, 1994, ed. by F. Leighton, M. Goodrich (ACM, New York, 1994), pp. 449–458. http://dl.acm.org/citation.cfm?id=195229

    Google Scholar 

  6. R. Borie, G. Parker, C. Tovey, Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families. Algorithmica 7, 555–581 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  7. R. Büchi, Weak second-order arithmetic and finite automata. Z. Math. Log. Grundl. Math. 6, 66–92 (1960)

    Article  MATH  Google Scholar 

  8. B. Courcelle, On context-free sets of graphs and their monadic second-order theory, in Graph-Grammars and Their Application to Computer Science 3rd International Workshop, Warrenton, Virginia, USA, December 2–6, 1986, ed. by H. Ehrig, M. Nagl, G. Rozenberg, A. Rosenfeld. LNCS, vol. 291 (Springer, Berlin, 1987), pp. 133–146

    Chapter  Google Scholar 

  9. B. Courcelle, The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  10. B. Courcelle, The monadic second-order logic of graphs. III. Tree-decompositions, minors and complexity issues. RAIRO Theor. Inform. Appl. 26(3), 257–286 (1992)

    MathSciNet  MATH  Google Scholar 

  11. B. Courcelle, The monadic second-order theory of graphs V: On closing the gap between definability and recognizability. Theor. Comput. Sci. 80, 153–202 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  12. B. Courcelle, The monadic second-order theory of graphs VI: On several representations of graphs by relational structures. Discrete Appl. Math. 54, 117–149 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  13. B. Courcelle, The monadic second-order theory of graphs VII: Graphs as relational structures. Theor. Comput. Sci. 101, 3–33 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  14. B. Courcelle, The monadic second-order theory of graphs VIII: Orientations. Ann. Pure Appl. Log. 72, 103–143 (1995)

    Article  MathSciNet  Google Scholar 

  15. B. Courcelle, The monadic second-order theory of graphs X: Linear orderings. Theor. Comput. Sci. 160, 87–144 (1996)

    Article  MathSciNet  Google Scholar 

  16. B. Courcelle, Basic notions of universal algebra for language theory and graph grammars. Theor. Comput. Sci. 163(1–2), 1–54 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  17. B. Courcelle, The expression of graph properties and graph transformations in monadic second-order logic, in Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1, ed. by G. Rozenberg (World Scientific, Singapore, 1997), pp. 313–400

    Chapter  Google Scholar 

  18. B. Courcelle, I. Durant, Automata for the verification of monadic second-order graph properties. J. Appl. Log. 10(4), 368–409 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  19. B. Courcelle, J. Engelfriet, Graph Structure and Monadic Second Order Logic: A Language-Theoretic Approach. Encyclopedia of Mathematics and Its Applications, vol. 138 (Cambridge University Press, Cambridge, 2012)

    Book  Google Scholar 

  20. B. Courcelle, P. Franchi-Zannettacci, Attribute grammars and recursive program schemes. Theor. Comput. Sci. 17, 163–191, 235–257 (1982)

    Google Scholar 

  21. B. Courcelle, M. Mosbah, Monadic second-order evaluations on tree-decomposable graphs. Theor. Comput. Sci. 109, 49–82 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  22. B. Courcelle, S. Oum, Vertex-minors, monadic second-order logic, and a conjecture of Seese. J. Comb. Theory, Ser. B 97(1), 91–126 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  23. M. Cygan, F. Fomin, E. van Leeuwin, Parameterized complexity of firefighting revisited, in Parameterized and Exact Computation, 6th International Symposium, IPEC ’11, Revised Selected Papers, Saarbrücken, Germany, September 6–8, 2011, ed. by D. Marx, P. Rossmanith. LNCS, vol. 7112 (Springer, Berlin, 2011), pp. 13–26

    Chapter  Google Scholar 

  24. E. Demaine, M. Hajiaghayi, Linearity of grid minors in treewidth with applications through bidimensionality. Combinatorica 28(1), 19–36 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  25. M. Fellows, F. Fomin, D. Lokshtanov, F. Rosamond, S. Saurabh, S. Szeider, C. Thomassen, On the complexity of some colorful problems parameterized by treewidth. Inf. Comput. 209(2), 143–153 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  26. J. Flum, M. Grohe, Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series (Springer, Berlin, 2006)

    Google Scholar 

  27. P. Golovach, D. Thilikos, Paths of bounded length and their cuts: parameterized complexity and algorithms, in Parameterized and Exact Computation, Proceedings of 4th International Workshop, IWPEC ’09, Copenhagen, Denmark, September 2009, ed. by J. Chen, F. Fomin. LNCS, vol. 5917 (Springer, Berlin, 2009), pp. 210–221

    Chapter  Google Scholar 

  28. Y. Gurevich, L. Harrington, Automata, trees and games, in Proceedings of 14th Annual ACM Symposium on Theory of Computing (STOC ’82), San Francisco, California, USA, May 5–May 7, 1982, ed. by H. Lewis, B. Simons, W. Burkhard, L. Landweber (ACM, New York, 1982), pp. 60–65

    Google Scholar 

  29. V. Kabanets, Recognizability equals definability for partial k-paths, Master’s thesis, Simon Fraser University, June 1996

    Google Scholar 

  30. V. Kabanets, Recognizability equals definability for partial k-paths, in Proceedings of 24th International Colloquium on Automata, Languages and Programming (ICALP 1997), Bologna, Italy, July 7–11, 1997, ed. by P. Degano, R. Gorrieri, A. Marchetti-Spaccamela. LNCS, vol. 1256 (Springer, Berlin, 1997), pp. 805–815

    Chapter  Google Scholar 

  31. D. Kaller, Definability equals recognizability for partial 3-trees, in Graph-Theoretic Concepts in Computer Science 22nd International Workshop, WG 1996, Revised Papers, Cadenabbia (Como), Italy, June 12–14, 1996, ed. by F. d’Amore, P.G. Franciosa, A. Marchetti-Spaccamela. LNCS, vol. 1197 (Springer, Berlin, 1997), pp. 239–253

    Google Scholar 

  32. J. Kneis, A. Langer, A Practical Approach to Courcelle’s Theorem. Electronic Notes in Theoretical Computer Science, vol. 251 (Elsevier, Amsterdam, 2009), pp. 65–81

    Google Scholar 

  33. J. Kneis, A. Langer, P. Rossmanith, Courcelle’s theorem—a game theoretic approach. Discrete Optim. 8(4), 568–594 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  34. A. Langer, F. Reidl, P. Rossmanith, S. Sikdar, Evaluation of an MSO-solver, in Proceedings of the Fourteenth Workshop on Algorithm Engineering and Experiments, ALENEX 2012, The Westin Miyako, Kyoto, Japan, January 16, 2012, ed. by D. Bader, P. Mutzel (SIAM/Omnipress, Philadelphia, 2012), pp. 55–63

    Google Scholar 

  35. A. Langer, P. Rossmanith, S. Sikdar, Linear-time algorithms for graphs of bounded rankwidth: a fresh look using game theory, in CoRR (Computing Research Repository, Berlin, submitted). arXiv:1102.0908

  36. D. Lapoire, Recognizability equals monadic second-order definability, for sets of graphs of bounded treewidth, in Proceedings of 15th Annual Symposium on Theoretical Aspects on Computer Science, STACS 98, Paris, France, February 1998, ed. by M. Morvan, C. Meinel, D. Krob. LNCS, vol. 1373 (Springer, Berlin, 1998), pp. 618–628

    Google Scholar 

  37. J. Makowsky, Algorithmic uses of the Feferman–Vaught theorem. Ann. Pure Appl. Log. 126, 159–213 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  38. A. Meier, J. Schmidt, M. Thomas, H. Vollmer, On the parameterized complexity of default logic and autoepistemic logic, in Language and Automata Theory and Applications, Proceedings of 6th International Conference, LATA 2012, A Coruña, Spain, March 5–9, 2012, ed. by A.-H. Dediu, C. Martín-Vide. LNCS, vol. 7183 (Springer, Berlin, 2012), pp. 389–400

    Google Scholar 

  39. M. Rabin, Decidability of second-order theories, and automata on infinite trees. Trans. Am. Math. Soc. 141, 1–35 (1969)

    MathSciNet  MATH  Google Scholar 

  40. N. Robertson, P. Seymour, Graph minors. V. Excluding a planar graph. J. Comb. Theory, Ser. B 41, 92–114 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  41. D. Seese, Entscheidbarkeits- und Interpretierbarkeitsfragen monadischer Theorien zweiter Stufe gewisser Klassen von Graphen, PhD thesis, Humboldt-Universitat, Berlin, 1976

    Google Scholar 

  42. D. Seese, The structure of models of decidable monadic theories of graphs. Ann. Pure Appl. Log. 53(2), 169–195 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  43. S. Shelah, The monadic theory of order. Ann. Math. (2) 102(3), 379–419 (1975)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Mathematics, Statistics and Operations Research, Victoria University, Wellington, New Zealand

    Rodney G. Downey

  2. School of Engineering and Information Technology, Charles Darwin University, Darwin, Northern Territory, Australia

    Michael R. Fellows

Authors
  1. Rodney G. Downey
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael R. Fellows
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag London

About this chapter

Cite this chapter

Downey, R.G., Fellows, M.R. (2013). Courcelle’s Theorem. In: Fundamentals of Parameterized Complexity. Texts in Computer Science. Springer, London. https://doi.org/10.1007/978-1-4471-5559-1_13

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-5559-1_13

  • Publisher Name: Springer, London

  • Print ISBN: 978-1-4471-5558-4

  • Online ISBN: 978-1-4471-5559-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation