arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2610.21379

Model Checking HyperRecHML is Decidable

Elli Anastasiadi·Kim Guldstrand Larsen·Martin Zimmermann
View original source ↗Read source document ↗Export metadata ↓

Abstract

Temporal hyperlogics combine explicit quantification over traces with temporal requirements evaluated over the quantified traces. HyperRecHML is a temporal hyperlogic which allows for arbitrary mixing of trace quantification and the use of fixed points for expressing temporal requirements, which makes it very expressive in comparison to other first-order hyperlogics. HyperRecHML has already been successfully applied in runtime verification, but the decidability of its model checking problem remains open. We answer this question positively by providing two main contributions. Firstly, a normalization procedure that allows to reduce arbitrary HyperRecHML formulas to a normal form with restricted nesting of trace quantification and fixed points. Secondly, we provide an automata-based model checking algorithm for formulas of this normal form. The complexity of our algorithm is comparable to similar ones for other hyperlogics, despite the extra expressive power.

Explore related subjects

cs.LOcs.FL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Elli Anastasiadi, Kim Guldstrand Larsen, Martin Zimmermann. 2026-10-15. Model Checking HyperRecHML is Decidable. https://arxiv.org/abs/2610.21379

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

KEEP EXPLORING

Related papers

arXiv2026

Overview and Roadmap of Team Automata

Team Automata is a formalism for interacting component-based systems proposed in 1997, whereby multiple sending and receiving actions from concurrent automata can synchronise. During the past 25+ years, team automata have been studied and applied in many different contexts, involving 25+ researchers and resulting in 25+ publications. In this paper, we first revisit the specific notion of synchronisation and composition of team automata, relating it to other relevant coordination models, such as Reo, BIP, Contract Automata, Choreography Automata, and Multi-Party Session Types. We then identify several aspects that have recently been investigated for team automata and related models. These include communication properties (which are the properties of interest?), realisability (how to decompose a global model into local components?), tool support (what has been automatised or implemented?), and variability (can a family of concrete product (automata) models be captured concisely?). Our presentation of these aspects provides a snapshot of the most recent trends in research on team automata, and delineates a roadmap for future research, both for team automata and for related formalisms.

cs.LO↗
arXiv2026

Derivatives for Containers in Univalent Foundations

Containers conveniently represent a wide class of inductive data types. Their derivatives compute representations of types of one-hole contexts, useful for implementing tree-traversal algorithms. Derivatives of discrete containers (whose positions have decidable equality) satisfy a universal property with respect to linear morphisms of containers. This induces a well-behaved notion of linear substitution for one-hole contexts. Working in Univalent Foundations, we extend the derivative operation to untruncated containers (whose shapes and positions are arbitrary types). We prove that this derivative, defined in terms of a set of isolated positions, satisfies an appropriate universal property in the wild category of untruncated containers and linear morphisms, as well as basic laws with respect to constants, sums and products. A chain rule exists, but is in general non-invertible. In fact, a globally invertible chain rule is inconsistent in the presence of non-set types, and equivalent to a classical principle when restricted to set-truncated containers. We derive a rule for derivatives of least fixpoints from the chain rule, and characterize its invertibility. All of our results are formalized in Cubical Agda.

cs.LO↗
arXiv2026

Algorithmic Unverifiability of Safety for Fixed and Recursively Self-Improving Systems

Existing impossibility results for AI verification concern a fixed system. Self-modifying systems (agents that rewrite their own code, recursive self-improvement loops) raise a different question: can a safety property that holds now be certified, in advance, to keep holding after the system rewrites itself? We model one step of self-modification as a total computable transformation of code, and preservation as 'safe now and safe after the step'. If the transformation depends only on behaviour, preservation is Rice's theorem one level up; if it reads the code, as self-modification does, preservation is no longer semantic, yet at least as hard as the halting problem, by the same s-m-n reduction carried out inside a class of behaviourally identical programs. One step is never harder than the property; persistence along the whole trajectory can be one arithmetical level higher. No tower of supervisors lowers the problem; every total supervisor errs on a set of systems it cannot locate. Every faithful scheme certifying on finite behavioural evidence admits, for properties not settled by any finite set of inputs, an evolution trace it certifies at every stage while the property is violated. Statically, we record the classical limits (Rice, Goedel, Trakhtenbrot) and add the resource face: over succinctly described finite environments, verifying a policy against an adversary is coNP-complete and synthesising one PSPACE-complete. These limits do not say self-modifying systems are unsafe; they locate where algorithmic guarantees break, at the expressivity a general system needs: Turing-completeness and unrestricted self-modification. What survives is exact: a monitor detects the first violation of a safety property, and no sound procedure certifies all safe systems; certification requires restricting rewrites by design; and a frozen reference keeps the question well posed.

cs.LO↗