https://arxiv.org/api/U7+U7sJFotF3Z+5vFHTgzPL+TRQ 2026-07-17T19:55:50Z 6096 0 15 http://arxiv.org/abs/2607.14983v1 2026-07-16T13:35:56Z

A VASS can be viewed as a finite-state automaton manipulating a fixed number (called its dimension) of counters holding non-negative values. The reachability problem, asking whether there is a run from one configuration, defined by a state and values of the counters, to another configuration, has been a long-standing algorithmic challenge in theoretical computer science. When the dimension is part of the input, the problem has been shown to be ACKERMANN-complete in 2021. For fixed dimension greater than 2, and in particular for dimension 3, the exact complexity of the reachability problem remains unclear. For a long time the known algorithms for the 3-dimensional VASS reachability problem had been non-elementary, while the best known lower bound is merely PSPACE hardness inherited from dimension 2. A recent breakthrough in (Czerwiński, Jecker, Lasota, Orlikowski, ICALP 2025) gave the first elementary upper bound for the problem, namely 2-EXPSPACE. In this paper it is shown that the reachability problem in 3-VASS belongs to EXPSPACE. The proof is based on a hierarchical pumpability analysis, yielding a doubly-exponential length bound on the shortest runs between two configurations.

2026-07-16T13:35:56Z 47 pages Weijun Chen Bo Fu Yuxi Fu Huan Long Chengfeng Xue Qizhe Yang Yangluo Zheng http://arxiv.org/abs/2607.14617v1 2026-07-16T06:30:51Z

Unordered trees are useful for modeling hierarchical structures in which the order among siblings is irrelevant. To represent flexible structural patterns in such data, unordered term tree patterns with height-constrained variables provide a natural framework. In our previous work, we studied the pattern matching problem for rooted unordered term tree patterns with height-constrained variables under the restriction that the child port of each variable must correspond to a leaf of a binding tree. In this paper, we remove this restriction and generalize the binding model so that the child port may correspond to any non-root vertex of a binding tree. Under generalized bindings, we formulate the corresponding membership problem and present a polynomial-time pattern matching algorithm. We also implement the proposed algorithm and conduct computational experiments to evaluate its running time. The experimental results show that the proposed method achieves practical running times.

2026-07-16T06:30:51Z 6 pages, 2 figures. Author preprint of a paper presented at ESKM 2026, IIAI-AAI 2026 Shintaro Matsushita Takayoshi Shoudai Yusuke Suzuki http://arxiv.org/abs/2607.12078v2 2026-07-15T20:51:12Z

We determine which digraphs admit an edge labeling by letters from a finite alphabet such that the resulting labeled digraph is a completely reachable automaton. Such digraphs are recognizable in polynomial time; however, the problem becomes NP-complete when the size of the label alphabet is fixed. We also classify the digraphs for which every edge labeling results in a completely reachable automaton.

2026-07-13T18:55:05Z 15 pages, 7 figures. In version 2, several inaccuracies are fixed and the proof of Lemma 5 is expanded Mikhail V. Volkov Yinfeng Zhu http://arxiv.org/abs/2603.15177v3 2026-07-15T19:40:49Z

We introduce and investigate the irreducibility of endomorphisms of finitely generated free semigroups, i.e., we investigate when an endomorphism $\varphi: Σ^+ \to Σ^+$, where $Σ$ is any alphabet, can be nontrivially expressed as a composition $\varphi = ψ_2 \circ ψ_1$ of endomorphisms $ψ_1, ψ_2: Σ^+ \to Σ^+$. We, hence, study a notion of primality in the endomorphism monoid of the free semigroup -- a natural and fundamental concept in this algebraic structure. We establish that irreducibility is a nontrivial property for the class of so-called rank-preserving endomorphisms, and we provide a characteristic condition separating the reducible and irreducible endomorphisms. We also characterise when an endomorphism is a factor of another endomorphism, analyse the non-uniqueness of factorisations of a rank-preserving endomorphism into its irreducible components, and investigate the use of incidence matrices to give insights into the (ir-)reducibility of rank-preserving endomorphisms.

2026-03-16T12:11:52Z Paul C. Bell Eva Foster Daniel Reidenbach http://arxiv.org/abs/2607.13981v1 2026-07-15T16:08:36Z

We study model checking for an epistemic metric temporal logic with past, interpreted over finite Büchi automata under synchronous perfect recall. The logic is motivated by observation-based verification problems such as diagnosis and opacity, where an observer sees only a projection of an execution and reasons about events that may have occurred earlier. These requirements use no alternation between different agents' knowledge. We therefore consider the agent-alternation-free fragment, in which nested knowledge operators must refer to the same agent. We show that model checking for this fragment is EXPSPACE-complete. The lower bound already holds with one agent, one occurrence of the knowledge operator, and no non-trivial metric bounds. For the upper bound, we combine temporal test automata with perfect-recall observers. Because past formulas may have different truth values on indistinguishable histories ending in the same system state, the observer must track temporal automaton states in addition to system states.

2026-07-15T16:08:36Z 31 pages Benedikt Bollig Matthias Függer Thomas Nowak Paul Zeinaty http://arxiv.org/abs/2607.13951v1 2026-07-15T15:39:50Z

We prove that the Post Correspondence Problem for finitely generated free groups is undecidable, even when one of the two homomorphisms is injective. This resolves a longstanding open problem in algorithmic group theory. The result exhibits a sharp contrast with the theory of fixed subgroups: although the equalizer of two free-group homomorphisms is finitely generated whenever one of the maps is injective, there is no algorithm that decides whether this equalizer is trivial. The proof proceeds through a connection with finite-state transducers. Given a cyclic tag system $\mathcal C$, we effectively construct a finite partial deterministic inverse transducer $\mathcal{T}_{\mathcal C}$ whose fixed-point set is nontrivial if and only if $\mathcal C$ halts. We then associate to any such transducer two homomorphisms \(g,h\colon F_Y\longrightarrow F_A,\) with $h$ injective, such that their equalizer is nontrivial precisely when the transducer has a nontrivial fixed loop. Consequently, the rank of these equalizers cannot be computed in general, answering a question posed by Stallings in 1984. As a further consequence, we prove that no algorithm computes a basis for the fixed subgroup of a virtual endomorphism of a finitely generated free group, nor constructs a finite automaton recognizing the reduced fixed-point language of a finite complete inverse transducer.

2026-07-15T15:39:50Z 18 pages, comments are welcome! André Carvalho http://arxiv.org/abs/2607.13782v1 2026-07-15T12:38:07Z

The goal of this paper is to propose a unifying model for Nerode-style characterizations of regularity across functions with different output domains. Building on Hauser's work in communication complexity, we generalize the setting by relaxing the computability assumptions and allowing non-Boolean output domains. We consider functions of type $Σ^* \to \domain$, where $Σ$ is a finite alphabet and $\domain$ is an arbitrary domain. For several domains, we show that the model coincides with known models of computation. We further conjecture that an analogous correspondence holds for other domains that currently lack a Nerode-style characterization of regularity, and we provide ample supporting evidence. In the model, an input string $w$ is split as $w = w_1 w_2$ and distributed between two cooperating parties, Alice and Bob, who exchange a constant number of messages to compute the value of the function. Each message is either an element of the output domain or a signal drawn from a finite set of signals, and the parties must produce the correct output for every admissible split $w = w_1 w_2$. We further extend the framework to infinite alphabets in the setting of nominal sets, and investigate its expressiveness on languages of words with atoms.

2026-07-15T12:38:07Z Omid Yaghoubi Mikołaj Bojańczyk Aliaume Lopez Rafał Stefański http://arxiv.org/abs/2607.00507v2 2026-07-15T09:37:38Z

Quantum contextuality is a vital non-classical resource, yet illuminating the precise mechanisms through which it enables unconditional computational advantages remains a challenge. We translate graph-theoretic formulations of contextuality into an unconditional quantum memory advantage for formal language recognition. We define a promise problem on an exclusivity graph $G$ where any classical finite automaton respecting exclusivity requires $N \ge χ(G)$ memory states, whereas a QFA requires a memory of dimension $d = ξ(G)$. The gap between these bounds isolates a structural, information-theoretic incompatibility between classical and quantum descriptions that we term \textit{representational contextuality}. For Boolean orthogonality graphs, this exacts an exponential classical memory penalty ($d=\mathcal{O}(n)$ vs $N=2^{Ω(n)}$). Finally, we demonstrate a sharp algorithmic phase transition: allowing the classical machine a finite confusability of mutually exclusive events reduces this exponential classical memory cost to $\mathcal{O}(n)$.

2026-07-01T06:42:59Z 12 pages, 4 figures total (includes Supplemental Material). v2: Main results tightened and extended to include bounded-error probabilistic automata and entropic bounds Shiroman Prakash http://arxiv.org/abs/2607.13598v1 2026-07-15T08:46:48Z

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.

2026-07-15T08:46:48Z Patricia Bouyer B Srivathsan Vaishnavi Vishwanath http://arxiv.org/abs/2509.02117v4 2026-07-14T14:01:58Z

We present a necessary condition for an infinite language to be multiple context-free, which we call a Substitution Lemma. We apply it to show a sample selection of languages are not multiple context-free, including the word problem of the group $F_2\times F_2$. We also show that groups with multiple context-free word problem have decidable rational subset membership problem. Our result contrasts with previous work showing that the standard pumping lemma for context-free languages cannot be generalised to multiple context-free languages, and that weak variants of generalised Ogden's lemma do not apply to multiple context-free languages.

2025-09-02T09:13:14Z 27 pages, 6 figures, 2 tables. Small edits made Andrew Duncan Murray Elder Lisa Frenkel Mengfan Lyu http://arxiv.org/abs/2508.19186v2 2026-07-14T10:51:53Z

Reactive obstacle avoidance methods often cause agents to become trapped in local minima, because they can often only reason one step ahead (i.e., the next action based on the current state). In this paper, we use model checking to achieve reactive multi-step planning and obstacle avoidance on an autonomous robot. Our small, purpose-built model checking algorithm generates plans in situ (within the robot's code) based on ``core'' knowledge and attention as found in biological agents. This is achieved in real-time using no pre-computed data on a low-powered device. Our approach is based on chaining temporary control systems that are spawned to counteract disturbances in the local environment which disrupt an autonomous agent from its preferred action (or resting state). We mitigate state-space explosion by relying on temporary snapshots of the immediate environment, restricting the number of states. Multi-step planning using counter-examples generated by depth-first search and a negated LTL path property is applied to scenarios involving a cul-de-sac and a free-standing obstacle. Empirical results and informal proofs of two fundamental properties demonstrate the effectiveness of our approach for the creation of efficient multi-step plans for local obstacle avoidance. We significantly improve performance compared to a purely reactive agent that can only plan one step ahead. Our approach is an instructional case study for the development of safe and reliable navigation in the context of autonomous vehicles. We believe it also has general application in navigation for mission-critical mobile robots.

2025-08-26T16:49:30Z 41 pages excluding references, 21 figures, submitted to Formal Aspects of Computing Christopher Chandler Bernd Porr Giulia Lafratta Alice Miller http://arxiv.org/abs/2607.12580v1 2026-07-14T09:50:02Z

Given a global specification as a trace-closed regular language, Zielonka's theorem provides a construction to synthesise a language equivalent distributed implementation represented as a deterministic asynchronous automaton (AA). The construction is notoriously complicated, which has led to a line of work that considers restrictions on the specifications or on the distributed architectures, with the objective of providing a conceptually simpler construction. A new construction has recently been provided for "fair" specifications, in which all processes participate regularly. In this work, we enhance this construction to enable deterministic finite-state automata (DFA) specifications with "connectedly communicating processes": there should be a constant delay d such that if two processes do not hear from one another after this delay, they will never hear from one another until the end of the run. This is a relaxation of the fairness constraint, in which some process may deliberately stop communicating with another one, e.g. a client-server architecture, where a client stops asking the server for a resource if it did not get any response from it after a while. Our construction results in an AA where every process has a number of local states that is polynomial in the number of states of the DFA, and where the only exponential explosion is related to the parameter d, and the separation depth of processes.

2026-07-14T09:50:02Z Béatrice Bérard Benjamin Monmege B Srivathsan Arnab Sur http://arxiv.org/abs/2607.13097v1 2026-07-14T05:46:22Z

Reaction systems have evolved into a rich family of computational models differing in their treatment of multiplicities, resource management, concurrency, and state evolution. We introduce a unified semantic framework based on interval structures and interval-based transformation systems. The framework decomposes operational semantics into independent resource, production, update, and execution strategies, providing a common basis for describing, comparing, and constructing reaction-system variants. We show that classical reaction systems, restricted reaction systems, multiset reaction systems, reaction systems with concentration, and resource-preserving multiset reaction systems are all recovered as instantiations of the framework. Quantitative reaction systems are accommodated through an additional preprocessing stage. We further demonstrate that the framework naturally extends beyond reaction systems to other computational models, including Petri nets. The proposed framework provides a common semantic foundation for existing models and a flexible basis for developing and analysing new computational formalisms.

2026-07-14T05:46:22Z Paolo Bottoni Anna Labella Ion Petre http://arxiv.org/abs/2607.12170v1 2026-07-13T21:31:23Z

Analysis algorithms for quantitative automata are complex and hard to validate. Existing approaches -- benchmarks, mutation testing, uniform random generation -- each fail to expose subtle implementation bugs. We present a framework that repeatedly 1) generates random quantitative automata that are non-degenerate by construction, 2) tests each against a target property, and 3) shrinks any violation to a local minimum, yielding a small, actionable counterexample. We implement the framework for parametric timed automata (PTA) and apply it to IMITATOR, a mature model checker for PTA, uncovering 5 previously unknown bugs, one of which was exposed by a counterexample with just 2 locations and 1 transition.

2026-07-13T21:31:23Z Submitted version. Published version available at doi.org/10.1007/978-3-032-30693-7_13 Theoretical Aspects of Software Engineering (TASE 2026), Lecture Notes in Computer Science, vol. 16697, Springer, pp. 188-205, 2026 Mikael Bisgaard Dahlsen-Jensen Aarhus University, Aarhus, Denmark Jaco van de Pol Aarhus University, Aarhus, Denmark 10.1007/978-3-032-30693-7_13 http://arxiv.org/abs/2410.23187v3 2026-07-13T14:38:00Z

We define the class of explorable automata on finite or infinite words. This is a generalization of History-Deterministic (HD) automata, where this time non-deterministic choices can be resolved by building finitely many simultaneous runs instead of just one. We show that recognizing HD parity automata of fixed index among explorable ones is in PTime, thereby giving a strong link between the two notions. We then show that recognizing explorable automata is ExpTime-complete, in the case of finite words or parity automata up to index [0, 2]. Additionally, we define the notion of ω-explorable automata on infinite words, where countably many runs can be used to resolve the non-deterministic choices. We show ExpTime-completeness for ω-explorability of automata on infinite words for the safety and coBüchi acceptance conditions. We finally characterize the expressivity of (ω-)explorable automata with respect to the parity index hierarchy.

2024-10-30T16:42:22Z Emile Hazard Olivier Idir Denis Kuperberg