Automata for the verification of monadic second-order graph properties

DOI10.1016/j.jal.2011.07.001zbMath1285.03049OpenAlexW2020861083MaRDI QIDQ1948277

Irène Durand, Bruno Courcelle

Publication date: 2 May 2013

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2011.07.001

zbMATH Keywords

graph algorithmmonadic second-order logicfixed-parameter tractabilityclique-widthautomatonfly-automaton

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Graph theory (including graph drawing) in computer science (68R10) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Related Items (14)

On enumerating minimal siphons in Petri nets using CLP and SAT solvers: theoretical and practical complexity ⋮ Fly-automata for checking monadic second-order properties of graphs of bounded tree-width ⋮ Grammars and clique-width bounds from split decompositions ⋮ On quasi-planar graphs: clique-width and logical description ⋮ From tree-decompositions to clique-width terms ⋮ Recognizable languages of arrows and cospans ⋮ On the model-checking of monadic second-order formulas with edge set quantifications ⋮ Unnamed Item ⋮ Practical algorithms for MSO model-checking on tree-decomposable graphs ⋮ The behavior of clique-width under graph operations and graph transformations ⋮ Fly-automata for checking \(\mathrm{MSO}_2\) graph properties ⋮ Fly-Automata, Their Properties and Applications ⋮ Computations by fly-automata beyond monadic second-order logic ⋮ A characterisation of clique-width through nested partitions

Uses Software

• Autowrite
• MONA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the model-checking of monadic second-order formulas with edge set quantifications
• The strong perfect graph theorem
• MSOL partitioning problems on graphs of bounded treewidth and clique-width
• \(H\)-join decomposable graphs and algorithms with runtime single exponential in rankwidth
• On parse trees and Myhill-Nerode-type tools for handling graphs of bounded rank-width
• The number of registers required for evaluating arithmetic expressions
• The complexity of first-order and monadic second-order logic revisited
• Linear time solvable optimization problems on graphs of bounded clique-width
• Upper bounds to the clique width of graphs
• Parametrized complexity theory.
• Recognizing Berge graphs
• Approximating clique-width and branch-width
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• Monadic datalog over finite structures of bounded treewidth
• $\mathbb F$ -Rank-Width of (Edge-Colored) Graphs
• Cosmological lower bound on the circuit complexity of a small problem in logic
• Clique-Width is NP-Complete
• The monadic second-order logic of graphs III : tree-decompositions, minors and complexity issues
• The Complexity of Translating Logic to Finite Automata
• ON THE CLIQUE-WIDTH OF SOME PERFECT GRAPH CLASSES
• The Generation of Optimal Code for Arithmetic Expressions
• Finding Branch-Decompositions and Rank-Decompositions

This page was built for publication: Automata for the verification of monadic second-order graph properties