Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic

Abstract:

We consider Polyadic Higher-Order Fixpoint Logic (PHFL), a modal fixpoint logic that is obtained as the merger of Higher-Order Fixpoint Logic and the Polyadic μ-Calculus, two formalisms which were originally introduced as expressive languages for program specification purposes. Polyadicity enables formulas to make assertions about tuples of states rather than states only. From Higher-Order Fixpoint Logic, PHFL inherits the ability to formalise properties using higher-order functions.

We consider PHFL in the setting of descriptive complexity theory: its fragment using no functions of higher-order is exactly the Polyadic mu Calculus, and it is known from Otto’s Theorem that it captures the bisimulation-invariant fragment of the complexity class P. We extend this result by showing that certain other fragments of PHFL capture the bisimulation-invariant fragments of other important complexity classes. We first show that EXPTIME in this sense is captured by the fragment using at most functions of order 1. We also give characterisations of PSPACE and NLOGSPACE by certain formulas of these two fragments which can be regarded as having tail-recursive functions only.

While many characterisations of complexity classes in descriptive complexity theory have been obtained as extensions of logics with low expressive power, the work we present here introduces a logic of very high expressive power and characterises complexity classes by fragments of this generic framework.

This work is a joint work with Martin Lange.