A Bisimulation-Invariance-Based Approach to the Separation of Polynomial Complexity Classes

TL;DR

The paper investigates whether the bisimulation-invariant fragment of $P$ can be separated from $NP$ and $PSPACE$ by leveraging Otto's result that such queries are definable in the polyadic μ-calculus $\mathcal{L}_{\mu}^{\omega}$. It introduces the notion of relative regularity to connect definability on graphs to regular tree languages via power-graph unfoldings, thereby translating complexity-separation questions into tree-language pumping problems. A key contribution is the algebraic and logical characterisation of power graphs through $d$-bisimulations and their definability in $\mathcal{L}_{\mu}^{2}$, enabling a polynomial-time handle on power-ness and providing a framework to test non-regularity relative to $\textsc{Power}_d$ for potential separations. The work outlines two concrete NP and PSpace constructions (1NonUnivNFA and 2NonUnivNFA) whose relative non-regularity would imply $P \neq NP$ and $P \neq PSpace$, respectively, while noting the substantial difficulties in proving such non-regularity and the broader implications for descriptive complexity. Overall, the approach offers a promising descriptive-complexity pathway to longstanding questions, distinct from order-based arguments, by focusing on bisimulation-invariant tree-structure expressiveness and regularity.

Abstract

We investigate the possibility to separate the bisimulation-invariant fragment of P from that of NP, resp. PSPACE. We build on Otto's Theorem stating that the bisimulation-invariant queries in P are exactly those that are definable in the polyadic mu-calculus, and use a known construction from model checking in order to reduce definability in the polyadic $μ$-calculus to definability in the ordinary modal mu-calculus within the class of so-called power graphs, giving rise to a notion of relative regularity. We give examples of certain bisimulation-invariant queries in NP, resp. PSPACE, and characterise their membership in P in terms of relative non-regularity of particular families of tree languages. A proof of non-regularity for all members of one such family would separate the corresponding class from P, but the combinatorial complexity involved in it is high. On the plus side, the step into the bisimulation-invariant world alleviates the order-problem that other approaches in descriptive complexity suffer from when studying the relationship between P and classes above.

Figures (4)

• Figure 1: Some known logical characterisations of standard complexity classes and bisimulation-invariant counterparts.
• Figure 2: $\mathcal{F}_{2}(\{a\},\{f\})$-graph that is the $2$-power of the $(\{a\},\{f\})$-graph in Ex. \ref{['exm:power']}.
• Figure 3: The operation of pumping in trees as described in Def. \ref{['def:pump']}.
• Figure 4: Tree unfolding of the graph $\mathcal{G}^2$ from Fig. \ref{['fig:power']}.

Theorems & Definitions (39)

• Theorem 1
• proof
• Proposition 2
• Proposition 3: Otto's Theorem Otto/99b
• Definition 4
• Example 5
• Proposition 6: AndersenPMC:1994LL-FICS12
• Example 7
• Lemma 8
• proof