Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Preliminaries Kapitel lesen Erstes Kapitel lesen

2013 | OriginalPaper | Buchkapitel

13. Courcelle’s Theorem

verfasst von : Rodney G. Downey, Michael R. Fellows

Erschienen in: Fundamentals of Parameterized Complexity

Verlag: Springer London

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Methods via Automata and Bounded Treewidth
Nächstes Kapitel More on Width-Metrics: Applications and Local Treewidth
Fußnoten
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
Note that this is in the large universe.
 
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
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
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
Kabanets [426] is an extended abstract and the full proof only appears in his masters thesis, Kabanets [425].
 
Literatur
4.
K. Abrahamson, M. Fellows, Cutset regularity beats well-quasi-ordering for bounded treewidth, Preprint (1989)
5.
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
43.
S. Arnborg, Efficient algorithms for combinatorial problems on graphs with bounded decomposability—a survey. BIT Numer. Math. 25(1), 2–23 (1985) MathSciNetCrossRefMATH
46.
87.
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
108.
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) MathSciNetCrossRefMATH
113.
R. Büchi, Weak second-order arithmetic and finite automata. Z. Math. Log. Grundl. Math. 6, 66–92 (1960) CrossRefMATH
166.
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 CrossRef
167.
B. Courcelle, The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput. 85(1), 12–75 (1990) MathSciNetCrossRefMATH
168.
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) MathSciNetMATH
169.
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) MathSciNetCrossRefMATH
170.
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) MathSciNetCrossRefMATH
171.
B. Courcelle, The monadic second-order theory of graphs VII: Graphs as relational structures. Theor. Comput. Sci. 101, 3–33 (1992) MathSciNetCrossRefMATH
172.
B. Courcelle, The monadic second-order theory of graphs VIII: Orientations. Ann. Pure Appl. Log. 72, 103–143 (1995) MathSciNetCrossRef
173.
B. Courcelle, The monadic second-order theory of graphs X: Linear orderings. Theor. Comput. Sci. 160, 87–144 (1996) MathSciNetCrossRef
174.
B. Courcelle, Basic notions of universal algebra for language theory and graph grammars. Theor. Comput. Sci. 163(1–2), 1–54 (1996) MathSciNetCrossRefMATH
175.
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 CrossRef
177.
B. Courcelle, I. Durant, Automata for the verification of monadic second-order graph properties. J. Appl. Log. 10(4), 368–409 (2012) MathSciNetCrossRefMATH
178.
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) CrossRef
179.
B. Courcelle, P. Franchi-Zannettacci, Attribute grammars and recursive program schemes. Theor. Comput. Sci. 17, 163–191, 235–257 (1982)
181.
B. Courcelle, M. Mosbah, Monadic second-order evaluations on tree-decomposable graphs. Theor. Comput. Sci. 109, 49–82 (1993) MathSciNetCrossRefMATH
183.
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) MathSciNetCrossRefMATH
187.
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 CrossRef
214.
E. Demaine, M. Hajiaghayi, Linearity of grid minors in treewidth with applications through bidimensionality. Combinatorica 28(1), 19–36 (2008) MathSciNetCrossRefMATH
286.
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) MathSciNetCrossRefMATH
312.
J. Flum, M. Grohe, Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series (Springer, Berlin, 2006)
349.
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 CrossRef
367.
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
425.
V. Kabanets, Recognizability equals definability for partial k-paths, Master’s thesis, Simon Fraser University, June 1996
426.
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 CrossRef
427.
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
451.
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
453.
J. Kneis, A. Langer, P. Rossmanith, Courcelle’s theorem—a game theoretic approach. Discrete Optim. 8(4), 568–594 (2011) MathSciNetCrossRefMATH
477.
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
478.
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
481.
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
507.
528.
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
568.
M. Rabin, Decidability of second-order theories, and automata on infinite trees. Trans. Am. Math. Soc. 141, 1–35 (1969) MathSciNetMATH
584.
611.
D. Seese, Entscheidbarkeits- und Interpretierbarkeitsfragen monadischer Theorien zweiter Stufe gewisser Klassen von Graphen, PhD thesis, Humboldt-Universitat, Berlin, 1976
612.
616.
Metadaten
Titel
Courcelle’s Theorem
verfasst von
Rodney G. Downey
Michael R. Fellows
Copyright-Jahr
2013
Verlag
Springer London
Buch
Fundamentals of Parameterized Complexity

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

Electronic ISBN: 978-1-4471-5559-1

Copyright-Jahr: 2013

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