Hardness of monadic second-order formulae over succinct graphs

TL;DR

This work studies MSO model-checking on graphs succinctly represented by Boolean circuits, revealing a hardness dichotomy: every cw-nontrivial MSO property is NP- or coNP-hard when evaluated on succinct graphs. The authors develop a finite-type, saturation-based framework featuring Ω_q (a saturating graph) and a pumping mechanism to construct hard instances and reduce SAT to Succinct-φ while preserving bounded cliquewidth. They also analyze cw-trivial formulas, proving that decidability of cw-triviality is nuanced and can be undecidable in general, with decidability depending on whether a cliquewidth bound is given as input. The results extend prior FO-based findings to MSO and connect logical expressiveness, graph representations, and complexity in the realm of automata networks and succinct encodings, highlighting limitations on exploiting succinct representations for efficient model-checking.

Abstract

Our main result is a succinct counterpoint to Courcelle's meta-theorem as follows: every cw-nontrivial monadic second-order (MSO) property is either NP-hard or coNP-hard over graphs given by succinct representations. Succint representations are Boolean circuits computing the adjacency relation. Cw-nontrivial properties are those which have infinitely many models and infinitely many countermodels with bounded cliquewidth. Moreover, we explore what happens when the cw-nontriviality condition is dropped and show that, under a reasonable complexity assumption, the previous dichotomy fails, even for questions expressible in first-order logic.

Figures (4)

• Figure 1: Example succinct representation of $G$ (left) as a Boolean circuit $C$ (right) on labels $\{0,\dots,14\}$, that is with $N=15$. Interpreting labels as binary numbers on 4 bits with the least significant bit on the right, there is an arc $(x,y)$ if and only if $y=\lfloor x/2 \rfloor+8$. We use a syntactic sugar "$=$" for Boolean equality $(a \wedge b) \vee (\neg a \wedge \neg b)$. Remark that generalizing this idea to construct a succinct representation of a binary tree on $2^n-1$ nodes requires circuits of size linear in $n$ (here $n=4$).
• Figure 2: Example of clique decomposition, with colors $C=\{0,1,2\}$ where $0$ is red, $1$ is blue, $2$ is green. Each node contains the corresponding $k$-colored graph, and the operation should easily be deduced from the arity. As an example, the join operation on the bottom right leading to a directed cycle of length two with blue nodes has $M=\{(1,1,R),(1,1,L)\}$.
• Figure 3: Proof of Proposition \ref{['pro:pump']}.
• Figure 4: Illustration of the permutation $f$ in Proposition \ref{['prop:reorg']}.

Theorems & Definitions (36)

• Theorem A
• Theorem B: Theorem 5.2 of ggpt21
• Theorem C
• Lemma 2.1: l04
• Lemma 2.2: Corollary 5.60 of courcellebook
• Theorem 3.1
• Proposition 4.1
• Lemma 4.2
• proof
• proof : Proof of Proposition \ref{['pro:saturating']}.