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

TL;DR

This paper explores the potential separation of polynomial complexity classes P, NP, and PSPACE within the bisimulation-invariant fragment, using logical and model checking techniques to characterize their definability and regularity properties.

Contribution

It introduces a novel approach based on bisimulation invariance and polyadic mu-calculus to analyze complexity class separations, providing new characterizations and insights.

Findings

Bisimulation-invariant queries in P are exactly those definable in the polyadic mu-calculus.

Certain NP and PSPACE queries are characterized by relative non-regularity of tree languages.

The approach reduces the order-problem in descriptive complexity when studying P versus higher classes.

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 $\mu$-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.