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.

翻译：我们研究了将P的双模拟不变片段与NP（以及PSPACE）的双模拟不变片段分离的可能性。我们的研究建立在奥特定理的基础上，该定理指出P中的双模拟不变查询恰好是那些可在多变量μ-演算中定义的查询。我们利用模型检测中的一个已知构造，将多变量$μ$-演算中的可定义性约化为在所谓幂图类中普通模态μ-演算的可定义性，从而产生相对正则性的概念。我们给出了NP（以及PSPACE）中某些双模拟不变查询的示例，并通过特定树语言族的相对非正则性来刻画它们属于P的条件。若能证明某个此类族中所有成员的非正则性，即可将相应类与P分离，但其中涉及的组合复杂度很高。从积极的角度看，进入双模拟不变世界缓解了描述复杂性中其他方法在研究P与更高类关系时所面临的阶次问题。