On the model-checking of monadic second-order formulas with edge set quantifications

AbstractWe extend clique-width to graphs with multiple edges. We obtain fixed-parameter tractable model-checking algorithms for certain monadic second-order graph properties that depend on the multiplicities of edges, with respect to this “new” clique-width. We define special tree-width, the variant of tree-width relative to tree-decompositions such that the boxes that contain a vertex are on a path originating from some fixed node. We study its main properties. This definition is motivated by the construction of finite automata associated with monadic second-order formulas using edge set quantifications. These automata yield fixed-parameter linear algorithms with respect to tree-width for the model-checking of these formulas. Their construction is much simpler for special tree-width than for tree-width, for reasons that we explain