Practical algorithms for MSO model-checking on tree-decomposable graphs

DOI10.1016/J.COSREV.2014.08.001zbMATH Open1302.68184OpenAlexW2158543468MaRDI QIDQ473216FDOQ473216

Authors: Alexander Langer, Felix Reidl, Peter Rossmanith, Somnath Sikdar 

Publication date: 24 November 2014

Published in: Computer Science Review (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.cosrev.2014.08.001

Recommendations

• A Practical Approach to Courcelle's Theorem
• scientific article; zbMATH DE number 4081531
• Easy problems for tree-decomposable graphs
• On the parameterized intractability of monadic second-order logic
• Courcelle's theorem -- a game-theoretic approach

zbMATH Keywords

monadic second-order logicCourcelle's theoremtree decompositions

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Graph algorithms (graph-theoretic aspects) (05C85) Graph theory (including graph drawing) in computer science (68R10) Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.) (05C70) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Cites Work

• Modest theory of short chains. I
• Title not available (Why is that?)
• Treewidth computations. II. Lower bounds
• Algorithmic uses of the Feferman-Vaught theorem
• On parse trees and Myhill-Nerode-type tools for handling graphs of bounded rank-width
• Polynomial-time recognition of clique-width \(\leq 3\) graphs
• Domino Treewidth
• A uniform method for proving lower bounds on the computational complexity of logical theories
• Graph operations characterizing rank-width
• Generation of polynomial-time algorithms for some optimization problems on tree-decomposable graphs
• All structured programs have small tree width and good register allocation
• Linear-time algorithms for graphs of bounded rankwidth: a fresh look using game theory (extended abstract)
• Linear-time computation of optimal subgraphs of decomposable graphs
• Combinatorial problems on series-parallel graphs
• Regularity and locality in \(k\)-terminal graphs
• Channel assignment on graphs of bounded treewidth
• Querying linguistic treebanks with monadic second-order logic in linear time
• Bounded treewidth as a key to tractability of knowledge representation and reasoning
• The station location problem on two intersecting lines
• On the parameterized intractability of monadic second-order logic
• Exact algorithms for a loading problem with bounded clique width
• Algorithmic meta theorems for circuit classes of constant and logarithmic depth
• Methods for algorithmic meta theorems
• The monadic second-order logic evaluation problem on finite colored trees: a database-theoretic approach
• Title not available (Why is that?)
• Linear-time computability of combinatorial problems on series-parallel graphs
• Title not available (Why is that?)
• Processor Efficient Parallel Algorithms for the Two Disjoint Paths Problem and for Finding a Kuratowski Homeomorph
• The Complexity of Translating Logic to Finite Automata
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Fly-automata, their properties and applications
• Evaluation of an MSO-Solver
• A combinatorial and logical approach to linear-time computability (extended abstract)
• Modified parameterized complexity theory
• Fast Counting with Bounded Treewidth
• Graph-Theoretic Concepts in Computer Science
• Algorithms and models for railway optimization.
• \texttt{Autowrite}: a tool for term rewrite systems and tree automata
• Title not available (Why is that?)
• Title not available (Why is that?)
• Graph theory
• Title not available (Why is that?)
• Graph minors. X: Obstructions to tree-decomposition
• Optimization, approximation, and complexity classes
• Graph searching and a min-max theorem for tree-width
• Title not available (Why is that?)
• The DLV system for knowledge representation and reasoning
• A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth
• A partial k-arboretum of graphs with bounded treewidth
• Which problems have strongly exponential complexity?
• Algorithmic meta-theorems for restrictions of treewidth
• Graph minors. XIII: The disjoint paths problem
• Linear time solvable optimization problems on graphs of bounded clique-width
• Upper bounds to the clique width of graphs
• Handle-rewriting hypergraph grammars
• Parametrized complexity theory.
• Tree-depth, subgraph coloring and homomorphism bounds
• Approximating clique-width and branch-width
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• A mathematical introduction to logic.
• Graph structure and monadic second-order logic. A language-theoretic approach
• Back and forth between logic and games
• Easy problems for tree-decomposable graphs
• Clique-width is NP-complete
• Complexity of Finding Embeddings in a k-Tree
• The Complexity of Enumeration and Reliability Problems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the clique-width of some perfect graph classes
• Title not available (Why is that?)
• On the Relationship Between Clique-Width and Treewidth
• Title not available (Why is that?)
• Solving Connectivity Problems Parameterized by Treewidth in Single Exponential Time
• Title not available (Why is that?)
• Efficient algorithms for combinatorial problems on graphs with bounded decomposability - a survey
• Linear time algorithms for NP-hard problems restricted to partial k- trees
• Automata for the verification of monadic second-order graph properties
• Query evaluation via tree-decompositions
• Graph minors. II. Algorithmic aspects of tree-width
• Courcelle's theorem -- a game-theoretic approach
• Title not available (Why is that?)
• (Meta) Kernelization
• Bidimensionality and kernels
• Monadic Datalog and the expressive power of languages for web information extraction
• On simple characterizations of k-trees
• Fixed parameter algorithms for DOMINATING SET and related problems on planar graphs
• When trees grow low: shrubs and fast \(\mathrm{MSO}_{1}\)
• Algorithmic meta-theorems
• Dynamic Programming on Tree Decompositions Using Generalised Fast Subset Convolution
• Title not available (Why is that?)
• Sparsity. Graphs, structures, and algorithms
• Title not available (Why is that?)
• The polynomial-time hierarchy
• Mathematical logic.
• Title not available (Why is that?)
• Twin-Cover: Beyond Vertex Cover in Parameterized Algorithmics
• Recontamination does not help to search a graph
• Graph minors. I. Excluding a forest
• Title not available (Why is that?)
• Weak Second‐Order Arithmetic and Finite Automata
• Title not available (Why is that?)
• A Linear Recognition Algorithm for Cographs
• Decision Problems of Finite Automata Design and Related Arithmetics
• Directed Nowhere Dense Classes of Graphs
• Generalized finite automata theory with an application to a decision problem of second-order logic
• Title not available (Why is that?)
• Boolean-width of graphs
• S-functions for graphs
• Deciding first-order properties of locally tree-decomposable structures
• Title not available (Why is that?)
• The number of labeled k-dimensional trees
• Treewidth computations. I: Upper bounds
• Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families
• The complexity of first-order and monadic second-order logic revisited
• Model-checking by infinite fly-automata
• Special tree-width and the verification of monadic second-order graph properties
• On the model-checking of monadic second-order formulas with edge set quantifications
• Computations by fly-automata beyond monadic second-order logic
• Monadic second-order evaluations on tree-decomposable graphs
• Testing branch-width
• Title not available (Why is that?)
• The NP-completeness column: an ongoing guide
• On nowhere dense graphs
• Logic, graphs, and algorithms
• Title not available (Why is that?)
• Finding Branch-Decompositions and Rank-Decompositions
• Tree acceptors and some of their applications
• Finding good decompositions for dynamic programming on dense graphs
• Lower bounds on the complexity of \(\mathrm{MSO}_1\) model-checking
• On the Parameterised Intractability of Monadic Second-Order Logic
• Title not available (Why is that?)
• The first order properties of products of algebraic systems
• On converting CNF to DNF
• Easy instances for model checking
• Monadic Datalog over finite structures of bounded treewidth
• Title not available (Why is that?)

Cited In (13)

• Lower bounds on the complexity of \(\mathsf{MSO}_1\) model-checking
• Title not available (Why is that?)
• Courcelle's theorem -- a game-theoretic approach
• Computing the clique-width of cactus graphs
• Complexity of the multilevel critical node problem
• The firebreak problem
• Transforming graph states using single-qubit operations
• The complexity of restricted star colouring
• Computations by fly-automata beyond monadic second-order logic
• Coalitional games induced by matching problems: complexity and islands of tractability for the Shapley value
• Extension complexity, MSO logic, and treewidth
• Fly-automata for checking \(\mathrm{MSO}_2\) graph properties
• Realizability and verification of MSC graphs

Uses Software

• Autowrite
• CPLEX
• MONA
• Treewidthlib
• Datalog

This page was built for publication: Practical algorithms for MSO model-checking on tree-decomposable graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q473216)