Undecidability of Reachability for Constraint Automata

Jakub Michaliszyn

Home/Archive/arXiv

arXiv · 2610.15875

Undecidability of Reachability for Constraint Automata

Jakub Michaliszyn

View original source ↗Read source document ↗Export metadata ↓

Abstract

We prove that reachability for constraint automata over finite binary words is undecidable. Eight registers suffice, with conjunctive guards using only equality, proper prefix, proper suffix, and infix incomparability, without word constants or concatenation. Finite-run nonemptiness, Buechi nonemptiness, and bounded Buechi nonemptiness are undecidable as consequences. For Boolean guards over equality, prefix, suffix, and prefix and suffix incomparability, Buechi nonemptiness is PSPACE-complete with arbitrarily many registers and word constants. The upper bound also allows positive infix atoms and yields PSPACE-completeness of prefix--suffix LTL satisfiability.

Explore related subjects

cs.FL

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Jakub Michaliszyn. 2026-10-11. Undecidability of Reachability for Constraint Automata. https://arxiv.org/abs/2610.15875

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

KEEP EXPLORING

Related papers

arXiv2026

The No Endmarker Theorem for One-Way Probabilistic Pushdown Automata

In various models of one-way pushdown automata, the explicit use of two designated endmarkers on a read-once input tape has proven to be extremely useful for making a conscious, final decision on the acceptance/rejection of each input word immediately after reading the right endmarker. With no endmarkers, by contrast, a machine must constantly stay in either accepting or rejecting states at any moment since it never notices the end of the input word. This situation, however, helps us analyze the behavior of the machine whose tape head makes the consecutive moves on all prefixes of a given extremely long input word. Since those two machine formulations have their own advantages, it is natural to ask whether the endmarkers are truly necessary to correctly recognize languages. In the deterministic and nondeterministic models, it is well-known that the endmarkers are removable without changing the acceptance/rejection criteria of each input word. This paper demonstrates that, for a more general model of one-way probabilistic pushdown automata, the endmarkers are always removable. This is proven by employing probabilistic transformations from an "endmarker" machine to an equivalent "no-endmarker" machine at the cost of double exponential stack-state complexity without compromising its error probability. By setting the machine's error probability appropriately, our proof also provides an alternative proof to both the deterministic and the nondeterministic models as well.

cs.FL↗

arXiv2026

Simple grammar bisimilarity, with an application to session type equivalence

We provide an algorithm for deciding simple grammar bisimilarity whose complexity is polynomial in the valuation of the grammar (maximum seminorm among production rules). Since the valuation is at most exponential in the size of the grammar, this gives rise to a (single) exponential running time. Previously only a double-exponential algorithm was known. As an application, we provide a conversion from context-free session types to simple grammars whose valuation is linear in the size of the type. In this way, we provide the first polynomial-time algorithm for deciding context-free session type equivalence.

cs.FL↗

arXiv2026

Semi-Linearity and Generalized Stratified Semi-Linearity beyond Context-Free Languages

Parikh's famous theorem relates to the semi-linearity of context-free languages. We seek for expanding the scope of the semi-linear property from context-free languages to languages beyond them. Of those languages, this work focuses on the languages that are particularly recognized by one-way nondeterministic depth-k storage automata under a natural restriction of frozen blank sensitivity. Those languages (which are called $k$-storable languages) have been already proven to satisfy a natural generalization of the well-known pumping lemmas for regular and context-free languages. The semi-linearity of k-storable languages generalizes Parikh's theorem on the semi-linearity of context-free languages. As for bounded languages, Ginsburg and Spanier's well-known theorem characterizes context-free languages in terms of stratified semi-linearity. This notion is further generalized and is used to characterize the k-storable languages as well. Such a generalization is interesting in its own right. This helps us take an abstract treatment of k-storable languages without relying on "machines". Our results strengthen the belief that those languages are "natural" generalizations of context-free languages.

cs.FL↗