Low rank MSO

TL;DR

This paper introduces low rank MSO, a restricted logic for graphs, and establishes its expressive power equivalences with other logics over specific graph classes, leading to polynomial-time decidability of properties.

Contribution

It defines low rank MSO and proves its expressive power matches other logics on certain graph classes, extending understanding of graph logic complexity.

Findings

Low rank MSO matches separator logic on weakly sparse graphs.

Low rank MSO matches flip-connectivity logic on graphs with bounded VC dimension.

Properties in low rank MSO are decidable in polynomial time.

Abstract

We introduce a new logic for describing properties of graphs, which we call low rank MSO. This is the fragment of monadic second-order logic in which set quantification is restricted to vertex sets of bounded cutrank. We prove the following statements about the expressive power of low rank MSO. - Over any class of graphs that is weakly sparse, low rank MSO has the same expressive power as separator logic. This equivalence does not hold over all graphs. - Over any class of graphs that has bounded VC dimension, low rank MSO has the same expressive power as flip-connectivity logic. This equivalence does not hold over all graphs. - Over all graphs, low rank MSO has the same expressive power as flip-reachability logic. Here, separator logic is an extension of first-order logic by basic predicates for checking connectivity, which was proposed by Boja\'nczyk [ArXiv 2107.13953] and by Schirrmacher, Siebertz, and Vigny [ACM ToCL 2023]. Flip-connectivity logic and flip-reachability logic are analogues of separator logic suited for non-sparse graphs, which we propose in this work. In particular, the last statement above implies that every property of undirected graphs expressible in low rank MSO can be decided in polynomial time.