Definability equals recognizability for graphs of bounded treewidth

2016/05/10 by Bojańczyk, Mikołaj, Pilipczuk, Michał · 4 citations
#Computational Complexity (cs.CC) #Data Structures and Algorithms (cs.DS) #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1605.03045

Abstract

We prove a conjecture of Courcelle, which states that a graph property is definable in MSO with modular counting predicates on graphs of constant treewidth if, and only if it is recognizable in the following sense: constant-width tree decompositions of graphs satisfying the property can be recognized by tree automata. While the forward implication is a classic fact known as Courcelle's theorem, the converse direction remained open

Cited by

• Homomorphism Indistinguishability, Multiplicity Automata Equivalence, and Polynomial Identity Testing
• The role of counting quantifiers in laminar set systems
• Finding sparse induced subgraphs on graphs of bounded induced matching treewidth
• Elimination Distance to Dominated Clusters

Related

• Definability Equals Recognizability for k-Outerplanar Graphs
• MSOL-Definability Equals Recognizability for Halin Graphs and Bounded Degree k-Outerplanar Graphs
• Courcelle's Theorem Without Logic
• Algorithmic Meta-Theorems for Graphs of Bounded Vertex Cover
• First Order Logic on Pathwidth Revisited Again