Fly-automata for checking MSO 2 graph properties

TL;DR

This paper develops fly-automata that can efficiently check MSO2 properties of graphs with bounded tree-width by leveraging their incidence graphs, enabling practical implementation of property verification.

Contribution

It adapts previous fly-automata techniques to MSO2 properties on graphs of bounded tree-width via incidence graphs, making the automata constructible and usable.

Findings

Automata can check MSO2 properties on bounded tree-width graphs.

Incidence graphs have linear clique-width in terms of tree-width.

Constructed automata are practical and implementable.

Abstract

A more descriptive but too long title would be : Constructing fly-automata to check properties of graphs of bounded tree-width expressed by monadic second-order formulas written with edge quantifications. Such properties are called MSO2 in short. Fly-automata (FA) run bottom-up on terms denoting graphs and compute "on the fly" the necessary states and transitions instead of looking into huge, actually unimplementable tables. In previous works, we have constructed FA that process terms denoting graphs of bounded clique-width, in order to check their monadic second-order (MSO) properties (expressed by formulas without edge quan-tifications). Here, we adapt these FA to incidence graphs, so that they can check MSO2 properties of graphs of bounded tree-width. This is possible because: (1) an MSO2 property of a graph is nothing but an MSO property of its incidence graph and (2) the clique-width of the incidence graph of a graph is linearly bounded in terms of its tree-width. Our constructions are actually implementable and usable. We detail concrete constructions of automata in this perspective.