Fly-automata for checking \(\mathrm{MSO}_2\) graph properties
type: Item
instance of: scholarly article
title: Fly-automata for checking \(\mathrm{MSO}_2\) graph properties
zbMATH Open document ID: 1445.03045
published in: Discrete Applied Mathematics
publication date: 2018-05-24T00:00:00Z
full work available at URL: https://arxiv.org/abs/1511.08605
review text: This paper shows how to construct on the fly automata to check monadic second-order properties with edge quantification, $\text{MSO}_2$, of bounded tree-width graphs, giving explicit automata for specific properties. More precisely, for a graph $G$ this paper considers its incidence graph $\mathrm{Inc}(G)$, which is a (bipartite) graph whose vertices are the vertices and the edges of $G$, its edge relation contains couples formed of an edge of $G$ and one of its ends, to which (in the non-directed case) a unary predicate distinguishing the vertices of $G$ is added. $\text{MSO}_2$ is then the usual monadic second-order logic, hence allowing both elements and sets quantifications, on the structure $\mathrm{Inc}(G)$. Both finite directed and undirected graphs are considered. Bounded tree-width graphs are represented by their construction terms under clique-width operations that use labels on vertices (one for vertices and one for edges), relabeling, disjoint union and adding an end vertex to an edge for specific labels. The paper builds on the results of \textit{B. Courcelle} and \textit{J. Engelfriet} [Graph structure and monadic second-order logic. A language-theoretic approach. Cambridge: Cambridge University Press (2012; Zbl 1257.68006); J. Appl. Log. 10, No. 4, 368--409 (2012; Zbl 1285.03049)] by introducing \textit{fly-automata}, which are tree automata that run bottom-up on terms denoting graphs, where instead of storing a transition table, states and transitions are computed, as needed, by (small) programs.
reviewed by: Roger Villemaire
Mathematics Subject Classification ID: 03D05
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 05C75
Mathematics Subject Classification ID: 68Q45
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 6872427
zbMATH Keywords: tree automata
zbMATH Keywords: graphs
zbMATH Keywords: bounded tree-width
zbMATH Keywords: monadic second-order logic
MaRDI profile type: MaRDI publication profile
OpenAlex ID: W2288162826
arXiv ID: 1511.08605
cites work: A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth
cites work: The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
cites work: On the model-checking of monadic second-order formulas with edge set quantifications
cites work: Fly-Automata, Their Properties and Applications
cites work: Automata for the verification of monadic second-order graph properties
cites work: Model-Checking by Infinite Fly-Automata
cites work: Computations by fly-automata beyond monadic second-order logic
cites work: Q3077955
cites work: Linear time solvable optimization problems on graphs of bounded clique-width
cites work: Q4503944
cites work: Fundamentals of parameterized complexity
cites work: Q5417642
cites work: The complexity of first-order and monadic second-order logic revisited
cites work: Q2766682
cites work: Courcelle's theorem -- a game-theoretic approach
cites work: Practical algorithms for MSO model-checking on tree-decomposable graphs
DOI: 10.1016/J.DAM.2016.10.018
Recommended article: Fly-automata for checking monadic second-order properties of graphs of bounded tree-width
Recommended article: Automata for the verification of monadic second-order graph properties
Recommended article: Computations by fly-automata beyond monadic second-order logic
Recommended article: Model-Checking by Infinite Fly-Automata
Recommended article: Fly-Automata, Their Properties and Applications
Recommended article: Special tree-width and the verification of monadic second-order graph properties
Recommended article: On the model-checking of monadic second-order formulas with edge set quantifications
Recommended article: Q4381404
Recommended article: Dynamic algorithms for graphs of bounded treewidth
author: Bruno Courcelle
description: scientific article