https://arxiv.org/api/ho461HqvkuIxZvdZrZXMauWisIA 2026-07-22T19:06:10Z 6102 90 15 http://arxiv.org/abs/2408.00750v4 2026-06-25T17:28:57Z

Christol and, independently, Denef and Lipshitz showed that an algebraic sequence of $p$-adic integers (or integers) is $p$-automatic when reduced modulo $p^α$. Previously, the best known bound on the minimal automaton size for such a sequence was doubly exponential in $α$. Under mild conditions, we improve this to a bound whose dominant factor is $p^{α^3 h d / 3}$, where $h$ and $d$ are the height and degree of the minimal annihilating polynomial modulo $p$. We achieve this bound by showing that all states in the automaton are naturally represented in a new numeration system. This significantly restricts the set of possible states. Since our approach embeds algebraic sequences as diagonals of rational functions, we also obtain bounds more generally for diagonals of multivariate rational functions.

2024-08-01T17:52:24Z 50 pages, 1 figure, 2 tables; publication version Eric Rowland Reem Yassawi http://arxiv.org/abs/2606.27209v1 2026-06-25T16:03:32Z

The probabilistic bisimilarity distance provides a quantitative measure of behavioural difference for labelled Markov chains, but it may be discontinuous under perturbations of the transition probabilities. This lack of continuity undermines its applicability to empirically derived models, where transition probabilities are often approximations. Recently, we (CAV 2025) introduced robust probabilistic bisimilarity as a sufficient condition for continuity at distance zero. In this paper, we show that it is also a necessary condition, that is, two states are robustly probabilistic bisimilar if and only if their probabilistic bisimilarity distance is small for any small enough perturbation of the transition probabilities. We further extend robustness to non-bisimilar state pairs to establish a complete characterization for continuity of the probabilistic bisimilarity distance. Based on this characterization, we develop a polynomial time algorithm to decide continuity. Finally, we complement our theoretical contributions with an experimental evaluation demonstrating the proposed approach in practice. Our results show that the extra step of deciding continuity requires minimal additional cost when compared to computing the probabilistic bisimilarity distance.

2026-06-25T16:03:32Z Accepted to the 37th International Conference on Concurrency Theory (CONCUR 2026) Syyeda Zainab Fatmi Stefan Kiefer David Parker Franck van Breugel http://arxiv.org/abs/2606.27172v1 2026-06-25T15:41:00Z

Parameterized verification of finite-state processes with rendez-vous synchronization is notoriously undecidable when processes are linearly ordered. In this paper we study two kinds of bounds under which we determine the complexity of safety checking over tree topologies. When bounding the depth we obtain that the complexity is related to the fast growing hierarchy. Our second bound limits the alternations between upwards and downwards synchronizations in the tree (phases), and occurs naturally in many concrete settings. If we fix the number of phases then the complexity of safety checking is EXPSPACE complete, and if the number of phases is part of the input it is 2EXPSPACE complete (both for arbitrary depth).

2026-06-25T15:41:00Z Full version of the paper with the same title and authors to appear in the proceedings of CONCUR 2026 Romain Delpy Anca Muscholl Grégoire Sutre http://arxiv.org/abs/2606.27166v1 2026-06-25T15:34:10Z

The reachability problem for Vector Addition Systems (VAS) is a central decision problem in the theory of infinite-state systems, first solved by Kosaraju and Mayr in the 1980s. An alternative, conceptually simpler approach introduced by Leroux shows that non-reachability is always witnessed by semilinear inductive invariants, yielding a decision procedure by combining an enumeration of runs with a search for such invariants. However, the construction of these invariants relies on a back-and-forth scheme that depends symmetrically on the source and the target. As a result, the invariants are not guaranteed to reflect the structural properties of the VAS, and the construction is difficult to extend to asymmetric models such as Branching VAS. We introduce a new forward-only construction of semilinear inductive invariants for VAS. Our method builds invariants from the source configuration alone and avoids the need for backward reasoning. This yields invariants that are more canonical and better aligned with the structure of the system. In particular, our method produces periodic inductive invariants for periodic VAS. Beyond its intrinsic interest, our approach provides a step toward extending invariant-based techniques to Branching VAS.

2026-06-25T15:34:10Z Full version of the paper with the same title and authors to appear in the proceedings of MFCS 2026 Clotilde Bizière Jérôme Leroux Grégoire Sutre http://arxiv.org/abs/2505.15290v2 2026-06-25T14:49:43Z

Despite its prevalence, probabilistic bisimilarity suffers from a lack of robustness under minuscule perturbations of the transition probabilities. This can lead to discontinuities in the probabilistic bisimilarity distance function, undermining its reliability in practical applications where transition probabilities are often approximations derived from experimental data. Motivated by this limitation, we introduce the notion of robust probabilistic bisimilarity for labelled Markov chains, which ensures the continuity of the probabilistic bisimilarity distance function. We also propose an efficient algorithm for computing robust probabilistic bisimilarity and show that it performs well in practice, as evidenced by our experimental results.

2025-05-21T09:20:46Z Accepted to the 37th International Conference on Computer Aided Verification (CAV) 2025 Syyeda Zainab Fatmi Stefan Kiefer David Parker Franck van Breugel 10.1007/978-3-031-98679-6_12 http://arxiv.org/abs/2606.26038v2 2026-06-25T10:11:48Z

We consider weighted automata over the tropical semiring $\mathbb{Z}_\infty(min, +)$. Recently, it was shown that determinisation is decidable; in this paper we focus on the complexity when the alphabet is unary. In 2001, Lombardy showed this problem is decidable, a close inspection of his proof yields a coNP upper bound on the complexity. Earlier Gaubert showed that every weighted automaton in this setting can be effectively turned into an equivalent union of deterministic weighted automata. We prove Gaubert's result efficiently, presenting it as a generalisation of Chrobak's normal form for unary NFA. In particular, we prove that the equivalent union of deterministic weighted automata can be represented by a weighted automaton of quadratic size in the size of the original one, and this representation can be computed in polynomial time. Building on this, we show that determinisation, and even register minimisation (which generalises determinisation), is coNP-complete. We complete the paper with observations that the boundedness problem is also coNP-complete by reductions with determinisation. Lastly, we provide evidence that all of these problems are not FPT (by proving $coW_1$-hardness) when parametrised by the number of deterministic automata in the union.

2026-06-24T17:13:53Z Full version of a CONCUR 2026 paper Shaull Almagor Ismaël Jecker Filip Mazowiecki Łukasz Orlikowski David Purser Henry Sinclair-Banks http://arxiv.org/abs/2606.27407v1 2026-06-25T08:34:09Z

We introduce the \emph{observational hierarchy}, a new axis of classification for formal languages, orthogonal to the Chomsky hierarchy. An observer is a function $O : Σ^* \to S$ that determines which information about the input is accessible to a computational system. The order-blind automaton, which perceives the input as a multiset of symbols rather than a sequence, constitutes the paradigmatic case. We prove that the class of languages recognisable by any machine equipped with such an observer coincides exactly with the permutation-closed languages. We then define a partial order on observers that induces a hierarchy of language classes parametrised not by the computational power of the machine, but by the structure of the observer. We prove that this hierarchy has the structure of a partial order with a diamond-shaped profile sub-lattice, comprising the length branch $O_\bot \prec O_{\mathrm{len}} \prec O_{\mathrm{prof}} \prec O_\top$ and the parity branch $O_\bot \prec O_{\mathrm{par}} \prec O_{\mathrm{prof}} \prec O_\top$, with $O_{\mathrm{len}}$ and $O_{\mathrm{par}}$ incomparable, and an infinite subsequence branch $O_\bot \prec O_1 \prec O_2 \prec \cdots \prec O_\top$, both converging to the complete observer. We prove that the observational hierarchy is strictly incomparable with the Chomsky hierarchy, and introduce the notion of \emph{observational complexity} of a language. We further define observer-parametrised complexity classes $\mathbf{P}_O$ and $\mathbf{NP}_O$, and show that computational hardness and structural blindness are two independent phenomena. In particular, $\mathbf{P}_{O_{\mathrm{prof}}} = \mathbf{NP}_{O_{\mathrm{prof}}}$ holds as a structural collapse strictly inside $\mathbf{P}$.

2026-06-25T08:34:09Z Fabio F. G. Buono http://arxiv.org/abs/2606.26685v1 2026-06-25T07:14:38Z

In the past literature, families of two-way finite automata and pushdown automata having limited state complexity (i.e., the total number of inner states) and stack-state complexity (i.e., the total number of inner states multiplied by the total number of strings "pushable" to a stack), have been studied in direct connection to (mainstream) space-bounded complexity classes equipped with Karp-Lipton style advice of limited size when all inputs given to the automata have bounded length. Here, we acknowledge two major factors -- size and ceiling -- of such families, which have a significant impact on the complexity of finite and pushdown automata families, where the "size" refers to (stack-)state complexity and the "ceiling" refers to an input's length bound. In this line of study, we further explore those effects caused by different sizes and ceilings.

2026-06-25T07:14:38Z In Proceedings NCMA 2026, arXiv:2606.25881 EPTCS 446, 2026, pp. 105-120 Tomoyuki Yamakami University of Fukui 10.4204/EPTCS.446.7 http://arxiv.org/abs/2606.26684v1 2026-06-25T07:14:22Z

Parallel Communicating Finite Automata (PCFA) are systems of several finite automata that can communicate by requesting the state of another automaton. As an attempt to make PCFA as defined in [8] and [2] more realistic, the non-forgetting model is introduced where automata retain their own states while querying. As in previous publications, several variants of these automata systems are considered. The computational capacity of the non-forgetting model is investigated and compared to ''forgetting'' systems and multi-head finite automata. It is shown that most variants of non-forgetting PCFA are as powerful as multi-head automata in the deterministic and nondeterministic cases where the number of automata equals the number of heads. The only exception is the special case of deterministic centralized systems in non-returning mode. Here, a strict inclusion is proved. In the course of this proving, a proof from [2] is completed. With that, this paper answers some questions for nfPCFA that are open for the classical ''forgetting'' case.

2026-06-25T07:14:22Z In Proceedings NCMA 2026, arXiv:2606.25881 EPTCS 446, 2026, pp. 89-103 Jana Schulz University of Potsdam 10.4204/EPTCS.446.6 http://arxiv.org/abs/2606.26683v1 2026-06-25T07:14:06Z

Finite automata with translucent input letters are a recent model of discontinuous input processing. Basically, classical finite automata are equipped with a translucency function that defines, depending on the state, the set of translucent input symbols. While processing the input, translucent symbols are skipped and only visible symbols are read and processed. It is distinguished between deterministic and nondeterministic models and, in addition, between returning and non-returning models. In the former case, the automaton restarts from the left end of the input after having consumed some visible symbol, whereas in the latter case the automaton restarts from the left end of the input when the right endmarker symbol is seen. Returning finite automata with translucent letters have been introduced by Nagy and Otto and its non-returning variant has been introduced by Mraz and Otto. Many results concerning the computational capacity, relations between deterministic and nondeterministic models, and relations between returning and non-returning models are known. Moreover, some results on closure properties and decidability questions have been obtained as well. However, some questions have still been open since many years. In this paper, we will give answers to some of these open questions. In particular, we show the non-closure under concatenation, Kleene star, reversal, and inverse homomorphism for the non-returning deterministic as well as nondeterministic model. We also obtain non-closure under inverse homomorphism for the returning deterministic and nondeterministic model. Finally, we investigate the emptiness problem for non-returning finite automata with translucent input letters and show the decidability of the problem in case of deterministic as well as nondeterministic automata.

2026-06-25T07:14:06Z In Proceedings NCMA 2026, arXiv:2606.25881 EPTCS 446, 2026, pp. 73-87 Martin Kutrib University of Giessen, Germany Andreas Malcher University of Giessen, Germany Matthias Wendlandt University of Giessen, Germany 10.4204/EPTCS.446.5 http://arxiv.org/abs/2606.26682v1 2026-06-25T07:13:50Z

In this paper, we continue the research on the power of contextual grammars with selection languages from subfamilies of the family of regular languages. We investigate infix-, prefix-, and suffix-free languages (referred to as idefix-free languages) and compare such language families to some other subregular families of languages (finite, monoidal, nilpotent, combinational, (symmetric) definite, ordered, non-counting, power-separating, commutative, circular, union-free, star, and comet languages). Further, we compare the families of the hierarchies obtained for external contextual grammars with the language families defined by these new types for the selection. In this way, we extend the existing hierarchies by new language families.

2026-06-25T07:13:50Z In Proceedings NCMA 2026, arXiv:2606.25881 EPTCS 446, 2026, pp. 53-71 Marvin Ködding PH Heidelberg Bianca Truthe Universität Giessen 10.4204/EPTCS.446.4 http://arxiv.org/abs/2606.26680v1 2026-06-25T07:13:34Z

We introduce and study a family of two-head finite automata called two head returning finite automata (2-HRFA) operating on rectangular arrays of picture languages, in which both heads move in opposite directions. We show that the class of picture languages accepted by 2-HRFA is incomparable with the class of languages generated by context-free matrix grammars (CFMG), while it forms a proper subset of the class of languages accepted by returning pushdown automata (RPDA). In addition, we define a constrained variant, both head stepping two head returning finite automata (B2-HRFA), in which both heads are required to move in a synchronized, stepwise fashion. We prove that the class of languages accepted by returning finite automata (RFA) is a proper subset of the class of languages accepted by B2-HRFA, which in turn is a proper subset of the class of languages accepted by 2-HRFA. Closure properties for both the families of languages accepted by 2-HRFA and B2-HRFA are also investigated.

2026-06-25T07:13:34Z In Proceedings NCMA 2026, arXiv:2606.25881 EPTCS 446, 2026, pp. 37-52 Henning Fernau Universität Trier, Germany Benedek Nagy Eszterhazy Karoly Catholic University, Eger, Hungary R. Jennifer Rose Madras Christian College Robinson Thamburaj Madras Christian College D. Gnanaraj Thomas Madras Christian College 10.4204/EPTCS.446.3 http://arxiv.org/abs/2606.26679v1 2026-06-25T07:13:19Z

Regular expressions with counting operations (c-regexes) offer a compact representation of repeating patterns by allowing numerical bounds to be added to subexpressions. Recent work introduced the counting-set data structure, which allows simultaneous updates of multiple counter values for efficient matching. However, this approach suffers from a performance bottleneck when counting-sets must be replicated due to the presence of branching transitions. We propose a sparse counting-set approach, which reduces the replication overhead by maintaining only essential counter values, thereby yielding a more efficient matching algorithm.

2026-06-25T07:13:19Z In Proceedings NCMA 2026, arXiv:2606.25881 EPTCS 446, 2026, pp. 19-36 Martin Berglund Umeå University Brink van der Merwe Stellenbosch University Sicheol Sung Yonsei University 10.4204/EPTCS.446.2 http://arxiv.org/abs/2606.26678v1 2026-06-25T07:13:03Z

Backtracking regular expression matchers are widely used due to their expressive power but may exhibit exponential worst-case matching time. Memoization provides a principled method for eliminating redundant computation and ensuring linear matching time, but full memoization is memory-intensive and impractical. We introduce the Minimum Feedback Node (MFN) memoization scheme, a selective memoization strategy based on computing a minimum feedback vertex set of an automaton. We establish relationships with existing memoization schemes and analyze their behaviour under both Thompson and Glushkov automaton constructions.

2026-06-25T07:13:03Z In Proceedings NCMA 2026, arXiv:2606.25881 EPTCS 446, 2026, pp. 1-17 Martin Berglund Umeå University Brink van der Merwe Stellenbosch University Iain le Roux Stellenbosch University 10.4204/EPTCS.446.1 http://arxiv.org/abs/2606.26677v1 2026-06-25T07:10:54Z

Langton's ant is a simple two-dimensional cellular automaton whose long-term behavior exhibits remarkable complexity. While it is known that the ant eventually escapes any finite connected region of the grid, the quantitative aspects of this escape remain poorly understood. In this paper, we study the escaping time of Langton's ant, defined as the maximum number of steps the ant can perform within a finite connected domain before leaving it. We establish general upper bounds on the escaping time as a function of the domain size, and derive improved bounds for rectangular domains. In particular, we obtain a factorial upper bound for square domains via an inductive decomposition argument. We also obtain linear upper bounds for rectangular domains of height two and three via a column-by-column analysis. More generally, for rectangular domains with a fixed height, we establish a polynomial upper bound in the number of columns. These results are complemented by exact values computed through an optimized simulation algorithm that exploits the geometric symmetries of the grid and employs a backtracking branching strategy to avoid exhaustive search over all color configurations. We also provide lower-bound constructions, proving that the linear upper bounds for rectangular domains of heights two and three are asymptotically optimal.

2026-06-25T07:10:54Z Kossi Roland Etse