Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.23725

Integer Reachability in Data VASS

Roland Guttenberg·Łukasz Kamiński·Sławomir Lasota
View original source ↗Read source document ↗Export metadata ↓

Abstract

Data Petri nets are an extension of plain Petri nets where, intuitively speaking, tokens carry data values, and transitions may perform equality tests on data values involved. Likewise, data vector addition systems with states (data VASS) are an extension of plain VASS, and equivalent to data Petri nets. The decidability status of the reachability problem in this model is an established and long-standing open question. In this paper we perform a major step towards resolving this question: we show decidability of the integer reachability problem, where the counters can drop below zero. Contrarily to plain VASS, where integer reachability reduces to integer linear programming, the setting of data VASS is significantly more complex, mostly due to the fact that the state spaces are not finite but orbit-finite (like in register automata). Our decision procedure combines an iterative refinement, resembling the KLM decomposition in plain VASS, with a termination argument via a novel way of bounding the number of data values appearing in the refinement. As corollaries, we deduce decidability of a number of decision problems concerning register automata and data Petri nets.

Explore related subjects

cs.FL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Roland Guttenberg, Łukasz Kamiński, Sławomir Lasota. 2026-10-16. Integer Reachability in Data VASS. https://arxiv.org/abs/2610.23725

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

KEEP EXPLORING

Related papers

arXiv2026

Model Checking for Noisy Toric Words

Toric words have recently gained attention as a means to model the behaviour of dynamical systems such as linear loops. This work is concerned with describing when the toric model is precise enough to decide whether the trace of a system is contained in an omega-regular language. Our contributions are threefold. (i) We use topological means to generalise a class of toric words by defining noise-robust dynamical systems and their sets of noisy traces. We prove that all noisy traces of a system are almost-periodic, and have the same set of recurrent factors. (ii) We apply the abstract techniques above to concrete sequences obtained as sign descriptions of real algebraic linear recurrence sequences (LRS), and show that the language-membership problem for sign descriptions of LRS with few dominant roots is decidable. (iii) We show that noisy traces of noise-robust dynamical systems are indistinguishable to a prefix-independent omega-regular language, and inclusion is decidable provided the common language of their recurrent factors is recursive. We incidentally obtain properties of prefix-independent omega-regular languages that may be of independent interest.

cs.FL↗
arXiv2026

Symmetric two-counter machines

Counter machines are a particularly simple, Turing-complete model of computation. We study the expressive power of nondeterministic 2-counter machines which are symmetric, in that their set of update transitions is invariant under swapping of counters. Our model is an extension of symmetric 2-VASS, in that we allow modifying both counters within a single transition. As the main result we demonstrate a dramatic impact of symmetry: we show that symmetric 2-counter machines are not Turing-complete, by proving decidability of their reachability problem. We conjecture that the decidability extends to machines with 3 or more counters that are symmetric, meaning the set of update transitions is invariant under any permutation of counters. We leave this problem open for machines with 3 and more counters, while identifying a frontier of the impact of symmetry: we prove undecidability for 3-counter machines invariant under the cyclic permutation group of order 3.

cs.FL↗
arXiv2026

The complexity of smooth words over binary alphabets

Smooth sequences over an alphabet of positive integers $\{a,b\}$ are sequences that are infinitely derivable, the emblematic example being the Oldenburger-Kolakoski sequence $κ$ over $\{1,2\}$. The main way to study their language is to consider a finite version of smooth sequences called smooth words. In this paper we prove that the smooth words are exactly the factors of smooth sequences and we make progress towards the conjecture that the complexity of smooth words over $\{a,b\}$ grows like $Θ\left(n^{\log(a+b)/\log((a+b)/2)}\right)$: we prove the lower bound over any alphabet and the upper bound over even alphabets, and we improve the known upper bound over odd and mixed alphabets. We also provide a dichotomy that links the language, the morphicity and the factor complexity of $κ$.

cs.FL↗