Computations by fly-automata beyond monadic second-order logic

• Parameterized algorithms based on automata.
• Infinite automata computing their transitions.
• Problems described in monadic second-order logic.
• Counting and other problems, not expressible in monadic second-order logic.

The validity of a monadic-second order (MS) expressible property can be checked in linear time on graphs of bounded tree-width or clique-width given with appropriate decompositions. This result is proved by constructing from the MS sentence expressing the property and an integer that bounds the tree-width or clique-width of the input graph, a finite automaton intended to run bottom-up on the algebraic term representing a decomposition of the input graph. As we cannot construct practically the transition tables of these automata because they are huge, we use fly-automata whose states and transitions are computed “on the fly”, only when needed for a particular input. Furthermore, we allow infinite sets of states and we equip automata with output functions. Thus, they can check properties that are not MS expressible and compute values, for example, the number of p-colorings of a graph. We obtain XP and FPT graph algorithms, parameterized by tree-width or clique-width. We show how to construct easily such algorithms by combining predefined automata for basic functions and properties. These combinations reflect the structure of the MS formula that specifies the property to check or the function to compute.