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

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

1. Problem Statement
The paper addresses the fundamental open problem of whether $P = NP$ (and by extension, $P = PSPACE$). While descriptive complexity theory has successfully characterized complexity classes like $NP$, $PSPACE$, and $ExpTime$ using logical formalisms (e.g., $NP = \exists SO$, $PSPACE = FO + PFP$), characterizing the class $P$ on general, unordered structures remains elusive. This difficulty is known as the "order problem": logical characterizations of $P$ typically require an explicit total order on the input structure, whereas computational problems in $P$ do not inherently possess such an order.

The authors investigate whether separating the bisimulation-invariant fragments of these complexity classes ($P/\sim$ vs. $NP/\sim$ and $P/\sim$ vs. $PSPACE/\sim$) offers a viable path to resolving the general $P=NP$ question. They posit that proving $P \neq NP$ is equivalent to proving $P/\sim \neq NP/\sim$, provided that the classes in question contain hard problems that are bisimulation-invariant.

2. Methodology and Theoretical Framework
The paper builds upon two established results from the literature:

1. Otto's Theorem [28]: The class of bisimulation-invariant queries computable in polynomial time ($P/\sim$) is exactly captured by the Polyadic $\mu$-Calculus ($L^\omega_\mu$).
2. Model Checking Reduction [4, 23]: The model checking problem for the polyadic $\mu$-calculus can be reduced to that of the ordinary (monadic) $\mu$-calculus ($L_\mu$) via a specific product construction known as "power graphs."

The authors combine these to develop a framework based on relative regularity:

• Reduction to Tree Languages: Since graphs and their tree unfoldings are bisimilar, definability in a bisimulation-invariant logic reduces to the definability of tree languages.
• Power Graphs: For a graph $G$, the $d$-th power $G^d$ is the asynchronous product of $d$ copies of $G$, enriched with "reset" transitions that return a component to the root.
• Monofication: A syntactic transformation converts a formula in the polyadic $\mu$-calculus (over $G$) into a formula in the ordinary $\mu$-calculus (over $G^d$).
• Relative Regularity: A tree language $L$ is defined as regular relative to a context language $R$ if there exists an $L_\mu$ formula that correctly distinguishes members of $L$ from non-members within $R$, while making arbitrary claims on trees outside $R$.

3. Key Contributions and Characterizations
The paper establishes that the separation of complexity classes can be reduced to proving the relative non-regularity of specific families of tree languages.

• Equivalence of Separation (Theorem 1): The paper proves that $P = NP$ if and only if $P/\sim = NP/\sim$, and similarly for $PSPACE$. This relies on the existence of bisimulation-invariant hard problems, specifically the non-universality problems for Non-deterministic Finite Automata (NFA) over one-letter ($1NonUnivNFA$) and two-letter ($2NonUnivNFA$) alphabets.
• Characterization of Power Graphs (Section 4): The authors provide two characterizations of graphs that are bisimilar to $d$-powers:
  1. Algebraic: Via a $d$-dimensional asynchronous bisimulation that satisfies "persistence" (actions in one component do not affect others) and the "reset property."
  2. Logical: Via definability in the dyadic $\mu$-calculus ($L^2_\mu$) using specific formulas ($\phi_{per}$, $\phi_{rst}$, $\phi_{pow}$).
• Relative Pumping Lemma (Lemma 13): The authors adapt the standard pumping lemma for regular tree languages to the context of relative regularity. They show that if a language $L$ is regular relative to $R$, then for any tree in $L \cap R$, one can pump a path segment such that the resulting tree remains in $L$ if it remains in $R$. This makes proving non-regularity significantly harder, as the pumping must be confined within the structural constraints of $R$ (the power graphs).

4. Main Results
The core results link the complexity separation to the non-regularity of tree languages derived from NFA non-universality problems:

• Theorem 26: $P \neq NP$ if and only if for all $d \ge 1$, the language $1NonUnivNFA_d$ (tree unfoldings of $d$-powers of graphs in $1NonUnivNFA$) is non-regular relative to $Power_d$ (the language of trees bisimilar to $d$-powers).
• Theorem 30: $P \neq PSPACE$ if and only if for all $d \ge 1$, the language $2NonUnivNFA_d$ is non-regular relative to $Power_d$.

The paper constructs these languages explicitly. For instance, $1NonUnivNFA_d$ consists of trees where, for every path, the sequence of actions in a specific component (ignoring resets) eventually leads to a state without the accepting color $f$.

5. Significance and Claims
The paper modestly claims to offer a new line of attack on the $P=NP$ problem, rather than a solution. Its significance lies in:

• Alleviating the Order Problem: By shifting the focus to bisimulation-invariant queries, the approach bypasses the need for total orders on structures, a major hurdle in previous descriptive complexity attempts to characterize $P$.
• Logical Expressiveness: It reframes the separation of complexity classes as a question of logical inexpressivity (specifically, the inability of the ordinary $\mu$-calculus to define certain tree languages relative to power graphs).
• Feasibility and Challenges: The authors acknowledge that while the theoretical reduction is established, the actual proof of relative non-regularity involves "high combinatorial complexity." They note that standard non-regularity proofs are insufficient; one must construct pumping arguments that strictly preserve the structural properties of power graphs.

The paper concludes that while the path is difficult, the characterization of power graphs (both algebraically and logically) provides the necessary tools to attempt such proofs. It also highlights an open gap in the literature: unlike other major complexity classes, a logical characterization for $NP/\sim$ is currently unknown, which remains a barrier to fully exploiting this bisimulation-invariant approach.