Finite Satisfiability of Two-Variable Logic with Arbitrarily Many Successors

Artur Jeż; Jakub Michaliszyn; Piotr Witkowski

Home/Archive/arXiv

arXiv · 2610.19943

Finite Satisfiability of Two-Variable Logic with Arbitrarily Many Successors

Artur Jeż·Jakub Michaliszyn·Piotr Witkowski

View original source ↗Read source document ↗Export metadata ↓

Abstract

We study finite satisfiability of two-variable first-order logic over structures equipped with an arbitrary finite number of independent successor relations of linear orders. The number of successor relations is part of the input, and the vocabulary may contain further unrestricted unary and binary relations. We prove decidability in deterministic doubly exponential space together with a triply exponential bound on the size of a smallest finite model. This settles the unrestricted finite case beyond two successors.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Artur Jeż, Jakub Michaliszyn, Piotr Witkowski. 2026-10-14. Finite Satisfiability of Two-Variable Logic with Arbitrarily Many Successors. https://arxiv.org/abs/2610.19943

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

Model Checking HyperRecHML is Decidable

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.

cs.LO↗