Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.15475

Capturing Bisimulation-Invariant Exponential-Space Complexity Classes

Florian Bruse·David Kronenberger·Martin Lange
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.LOcs.CC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Florian Bruse, David Kronenberger, Martin Lange. 2026-10-11. Capturing Bisimulation-Invariant Exponential-Space Complexity Classes. https://doi.org/10.4204/eptcs.454.5

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Simple Obligation to Metric Interval Temporal Logic

Satisfiability of Metric Interval Temporal Logic (MITL) is a widely investigated subject. In this work, we present a new, and arguably simpler, approach for MITL satisfiability, based on an idea of tracking time-constrained obligations along a word. To check whether a Linear Temporal Logic (LTL) formula is true at a position of a word, it is natural to generate certain obligations that need to be satisfied at a later point. For instance, $a ~\mathcal{U}~ b$ (with strict Until semantics) is true at position $i$ if either $b$ or the set $\{a, a ~\mathcal{U}~ b\}$ is true at $i+1$. We enhance this idea in the context of MITL by introducing a notion of time inside these obligations. However, a naïve procedure could lead to more and more obligations getting generated along the word, with no bound on the number. We propose a simple mechanism to eliminate or merge redundant obligations. For MITL, this mechanism ensures that only a bounded number of obligations are maintained along the entire timed word. We develop this observation into a symbolic procedure for MITL satisfiability using regions.

cs.LO↗
arXiv2026

Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes

The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzmüller and Scott's Notes on Gödel's and Scott's variants of the ontological argument, reaches beyond the modal object language: its property quantifiers range over domains containing the nominals and satisfaction operators of hybrid logic. A proof using one proves a theorem of the embedding, not necessarily of the modal logic. That the framework affords this is not new. Whether a result is one of the modal logic can be settled by replaying it in an explicit calculus, one result at a time. More cheaply, and for all results at once, it can be approached by analysing what the embedding's proofs substitute. Every statement the Notes prove has a proof in the embedding substituting nothing outside the object language: 294 of them explicit proofs, machine-checked, none using a nominal. The Notes' own proofs substitute none either; what the check flags are terms a prover introduced. The three questions the Notes leave open are settled too, without nominals, but by the empty instance of the conjunction axiom, too cheaply to convince. As the Notes generalise it, to cover Gödel's "any number of summands", the axiom covers the empty conjunction and the singleton. This article restricts it to at least two different conjuncts, a non-degenerate reading of Gödel's footnote, and settles the questions again, without nominals. In effect the restriction excludes only the empty conjunction; the one-element case comes back with the other axioms. In one of the three variants the restriction refutes the possible existence of a God-like being; the answers return, with no side condition, once the Notes' non-emptiness clause is confined to Gödel's essence. Every theorem stated here is verified in Isabelle/HOL and independently in Lean 4; the countermodels are Nitpick's, checked by the build.

cs.LO↗
arXiv2026

Certifying Almost-Sure Reachability in Unknown MDPs

{\em Specification-Guided Reinforcement Learning (RL)} has largely concerned itself with \emph{learning} an optimal policy against a formal specification in an unknown {\em Markov Decision Process (MDP)}. We take up the dual question. Given a policy already in hand, can one \emph{verify} that it is correct against a formal specification in an unknown MDP, using sampling access alone? Such a question arises naturally in safety-critical systems. We investigate it for the {\em almost-sure reachability property}, whose correctness is witnessed by a {\em ranking supermartingale (RSM)} certificate. Our first finding is negative. In the absence of any further information about the MDP, one can neither learn such a certificate nor verify a candidate one with probabilistic guarantees. On the positive side, we show that, under a mild restriction, a known lower bound $p_{\min}$ on nonzero transition probabilities, a correct certificate \emph{can} be learned with PAC-style guarantees. To the best of our knowledge, this is the first study of learning and verifying certificates for almost-sure reachability in unknown MDPs from sampling access alone. Finally, our experiments show that the $p_{\min}$-based sufficient condition, while sound, is conservative: the learned certificate often remains valid on the true MDP even when the condition fails.

cs.LO↗