Capturing Bisimulation-Invariant Exponential-Space Complexity Classes

Otto's Theorem characterises the bisimulation-invariant PTIME queries over graphs as exactly those that can be formulated in the polyadic µ-calculus.This extends to a characterisation of the full bisimulation-invariant exponential-time hierarchy, using a higher-order extension of the polyadic µ-calculus, called PHFL, which is naturally stratified by type order.The bisimulation-invariant fragment of k-EXPTIME is captured by the fragment of PHFL whose formulas have type order at most k.This is obtained using a generalisation of the Immerman-Vardi Theorem by Freire and Martins.Here we provide such a characterisation of the exponential-space hierarchy.We show that the bisimulation-invariant fragment of k-EXPSPACE is captured by the fragment of PHFL of type order k + 1 whose formulas are tail-recursive.Tail recursion limits the interplay between fixpoints and higher-order functions so that model checking based on fixpoint iteration can be made more space efficient in a way comparable to tail recursion in programming languages.The capturing result makes use of a generalisation of Vardi's characterisation of PSPACE as first-order logic with partial fixpoints, namely that k-EXPSPACE is captured by higher-order logic of order k + 1 with partial fixpoints.