Bisimulation invariant logic captures exponential space complexity classes
Capturing Bisimulation-Invariant Exponential-Space Complexity Classes
Logic in Computer ScienceComputational Complexity
Summary
Computers can be asked complex questions about graphs, and some of these questions can be answered using special logical formulas. Previous work described how certain types of logic match problems solvable in a certain amount of time. This paper extends that idea to even harder problems that need more memory space, linking them to a new kind of logical formulas that are more limited in how they repeat themselves. The result helps understand which logical statements correspond exactly to these complex problems.
What this means in practice
- •For software verification engineers: Use the characterization to optimize verification of system properties that involve complex state spaces with tight memory constraints.
- •For database query optimizers: Inform design of query languages and optimization for graph databases by understanding exact logical boundaries of query complexity with memory limits.
A theory result. No direct application yet.
Authors
Florian Bruse, David Kronenberger, Martin Lange
Abstract
Otto's Theorem characterises the bisimulation-invariant PTIME queries over graphs as exactly those that can be formulated in the polyadic mu-calculus. This extends to a characterisation of the full bisimulation-invariant exponential-time hierarchy, using a higher-order extension of the polyadic mu-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.