Fly-automata for checking \(\mathrm{MSO}_2\) graph properties (Q1752502)

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.