https://arxiv.org/api/S6+5CNKs5gLk2Q7zL3poqr3qETA 2026-07-21T14:01:38Z 6101 75 15 http://arxiv.org/abs/2605.04657v2 2026-06-29T06:35:24Z

We introduce a novel logic for the specification of context-free hyperproperties, which capture, e.g., the flow of information in security-critical recursive systems. Intuitively, the logic extends visibly pushdown automata by quantification over traces, just like HyperLTL, the most important logic for regular hyperproperties, extends LTL by quantification over traces. Using a game-based approach, we show that model-checking is decidable for formulas with a single quantifier alternation, provided the stack height of the visibly pushdown automaton only depends on the traces bound to the variables of the first quantifier block. A single quantifier alternation suffices to express many information-flow properties studied in the literature. Complementarily, we show that model-checking is undecidable for formulas with a single quantifier alternation, if the stack behavior of the visibly pushdown automaton may depend on the second quantifier block. This also implies that model-checking is undecidable for almost all fragments with more than one quantifier alternation.

2026-05-06T09:02:53Z Sarah Winter Martin Zimmermann http://arxiv.org/abs/2604.25398v2 2026-06-29T06:15:25Z

We study bounded deviation of non-deterministic finite transducers under the Hamming distance: the bounded comparison problem asks, given two transducers and $k \in \mathbb{N}$, whether for every input the two transducers produce words at Hamming distance at most $k$. This problem is known to be decidable in polynomial time when $k$ is fixed, and in co-NP otherwise. We show that the problem is NL-complete when $k$ is fixed, co-NP-complete when $k$ is given in binary, and it is DP-complete to decide if the distance is exactly $k$. We also prove that if the two transducers have bounded comparison, then the maximal distance is at most quadratic in the size of both transducers, and that this bound is asymptotically tight. We prove the results on deviations problem, which asks similar questions on the distance of the pairs of input and output of a single transducer, and show that these two families of problems are logspace many-one equivalent.

2026-04-28T09:08:53Z 21 pages, 7 figures Luc Dartois Pierre-Cyrille Héam Ismaël Jecker Silvio Vescovo http://arxiv.org/abs/2302.13116v5 2026-06-29T03:51:48Z

We study the question of which visibly pushdown languages (VPLs) are in the complexity class $\mathsf{AC}^0$ and how to effectively decide this question. Our contribution is to introduce a particular subclass of one-turn VPLs, called intermediate VPLs, for which the raised question is entirely unclear: to the best of our knowledge our research community is unaware of containment or non-containment in $\mathsf{AC}^0$ for any language in our newly introduced class. Our main result states that there is an algorithm that, given a visibly pushdown automaton, correctly outputs exactly one of the following: that its language $L$ is in $\mathsf{AC}^0$, some $m\geq 2$ such that $L$ is $\mathsf{ACC}^0(m)$-hard (implying that $L$ is not in $\mathsf{AC}^0$), or a finite disjoint union of intermediate VPLs that $L$ is constant-depth equivalent to. In the latter of the three cases one can moreover effectively compute $k,l\in\mathbb{N}_{>0}$ with $k\not=l$ such that the concrete intermediate VPL $L(S\rightarrow \varepsilon\mid a c^{k-1} S b_1\mid ac^{l-1}Sb_2)$ is constant-depth reducible to the language $L$. Due to their particular nature we conjecture that either all intermediate VPLs are in $\mathsf{AC}^0$ or all are not. As a corollary of our main result we obtain that in case the input language is a visibly counter language our algorithm can effectively determine if it is in $\mathsf{AC}^0$ - hence our main result generalizes a result by Krebs et al. stating that it is decidable if a given visibly counter language is in $\mathsf{AC}^0$ (when restricted to well-matched words). For our proofs we revisit so-called Ext-algebras (introduced by Czarnetzki et al.), which are closely related to forest algebras (introduced by Bojańczyk and Walukiewicz), and use Green's relations.

2023-02-25T16:41:58Z 78 pages, to be published into the special issue of STACS 2024 Stefan Göller Nathan Grosshans http://arxiv.org/abs/2601.12621v2 2026-06-29T01:23:03Z

It is well known that computing a minimum deterministic finite automaton consistent with a given set of positive and negative examples is NP-hard. Previous work has identified conditions on the input sample under which the problem becomes tractable or remains hard. In this paper, we study the computational complexity of the case where the input sample is prefix-closed. This formulation is equivalent to computing a minimum Moore machine consistent with observations along its runs. We show that the problem is NP-hard to approximate when the sample set consists of all prefixes of binary strings. Furthermore, we show that the problem remains NP-hard as a decision problem even when the sample set consists of the prefixes of a single binary string. Our argument also extends to the corresponding problem for Mealy machines.

2026-01-18T23:28:36Z 12 pages, 4 figures Radu Cosmin Dumitru Ryo Yoshinaka Ayumi Shinohara http://arxiv.org/abs/2606.29595v1 2026-06-28T20:36:06Z

Mossel and Peres (2005) established a comprehensive framework for designing Bernoulli factories. Notably, they demonstrated that a single-variable function admits a finite-automata Bernoulli factory if and only if it is a rational function. Their Theorem 2.9 claims an extension of this result to multivariable functions, but it contains a subtle technical oversight in the application of Pólya's Theorem. We provide a direct counterexample: a rational function in three variables that admits a general Bernoulli factory but cannot be implemented by a finite-automata Bernoulli factory.

2026-06-28T20:36:06Z Renato Paes Leme Jon Schneider http://arxiv.org/abs/2310.09115v2 2026-06-28T14:42:33Z

Nondeterministic Discounted-Sum Automata (NDAs) are nondeterministic finite automata equipped with a discounting factor $λ>1$, and whose transitions are labelled by weights. The value of a run of an NDA is the discounted sum of the edge weights, where the $i$-th weight is divided by $λ^{i}$. NDAs are a useful tool for modelling systems where the values of future events are less influential than immediate ones. While several problems are undecidable or open for NDA, their deterministic fragment (DDA) admits more tractable algorithms. Therefore, determinization of NDAs (i.e., deciding if an NDA has a functionally-equivalent DDA) is desirable. Previous works establish that when $λ\in \mathbb{N}$, then every complete NDA, namely an NDA whose states are all accepting and its transition function is complete, is determinizable. This, however, no longer holds when the completeness assumption is dropped. We show that the problem of whether an NDA has an equivalent DDA is decidable when $λ\in \mathbb{N}$.

2023-10-13T14:00:54Z Shaull Almagor Neta Dafni http://arxiv.org/abs/2606.29405v1 2026-06-28T13:59:57Z

Finite-state transducers and Wheeler automata are two well-established frameworks in formal language theory. While transducers extend finite-state automata by associating output words to input words, Wheeler automata are automata whose underlying graph admits a co-lexicographic sorting of states, giving rise to the class of Wheeler languages, a proper subclass of star-free regular languages with efficient indexing properties. In this work, we introduce the notion of sequential Wheeler transducers, a class of deterministic one-way transducers combining the Wheeler condition on the underlying automaton with a monotonicity requirement on the output function. We establish several fundamental properties of this class: closure under composition, and closure of Wheeler languages under inverse image of Wheeler transductions. We then develop a minimization theory by refining Choffrut's syntactic equivalence $\sim_f$ into a relation $\sim_f^c$, and prove a Myhill-Nerode-style theorem characterizing exactly the functions realizable by a sequential Wheeler transducer. Finally, we give a machine-independent characterization of Wheeler functions in terms of the behavior of the function. These results lay the groundwork for a broader structural theory of Wheeler transducers, and we outline open problems concerning decidability, complexity, non-deterministic extensions, and logical characterizations.

2026-06-28T13:59:57Z Giovanna D'Agostino Andrea Paradiso http://arxiv.org/abs/2606.26768v2 2026-06-26T20:29:16Z

Büchi elevator automata naturally appear in several areas of formal methods as a structural expressibly-equivalent subclass of Büchi automata where every strongly connected component is either deterministic or inherently weak. It was shown that this class contains the majority of Büchi automata generated in practical applications, including LTL model-checking and verification of hyperproperties. Moreover, the elevator subclass enables more efficient complementation and determinization algorithms than unrestricted Büchi automata. In this paper, we introduce Emerson-Lei elevator automata, which is a generalization of Büchi elevator automata to richer acceptance conditions. We provide a complementation algorithm with a significantly better asymptotic complexity than the best known algorithm for unrestricted Emerson-Lei automata. The practical efficiency of our algorithm is demonstrated by an experimental comparison with the popular state-of-the-art tool Spot. Our work is, to the best of our knowledge, the first step towards practical algorithms for complementing, determinizing, and testing universality and inclusion of Emerson-Lei automata with rich acceptance conditions.

2026-06-25T08:50:49Z Accepted at CONCUR'26 Ondrej Alexaj Vojtěch Havlena Ondřej Lengál Yong Li Nicolas Mazzocchi http://arxiv.org/abs/2606.21976v2 2026-06-26T13:50:05Z

Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes $ω$-regular languages by processing their ultimately periodic words. FDFA are known to enjoy many good properties and can be exponentially more succinct than deterministic $ω$-automata with Rabin, Streett or parity acceptance. This paper addresses two main questions: (1) Are FDFA suitable for probabilistic model checking purposes? and (2) Is it possible to obtain an even more compact representation of $ω$-regular languages by allowing the components of an FDFA to be unambiguous instead of deterministic? Question (1) is answered in the affirmative by presenting the first polynomial-time algorithm for computing the probability that a discrete-time Markov chain satisfies an $ω$-regular property represented as an FDFA. Question (2) is motivated by the fact that unambiguous finite automata may require exponentially fewer states than deterministic ones. This paper introduces a model of families of unambiguous finite automata (FUFA) that captures the class of $ω$-regular languages. FUFA can be exponentially more succinct than both FDFA and unambiguous Büchi automata, and there is a single-exponential translation from linear temporal logic (LTL) to FUFA. This stands in contrast to a double-exponential lower bound for the translation from LTL to FDFA. Moreover, the polynomial-time probabilistic model checking algorithm for discrete-time Markov chains against FDFA-specifications is extended to the case where the property is represented by an FUFA with a deterministic leading automaton.

2026-06-20T10:18:32Z Full version of a paper accepted for publication at CONCUR 2026 Christel Baier Sascha Klüppelholz Timm Spork http://arxiv.org/abs/2604.25619v2 2026-06-26T12:38:38Z

Minimizing the size of finite automata is a fundamental problem in theoretical computer science. Beyond standard minimization, further reductions can be achieved by decomposing an automaton into smaller components whose languages combine via intersection or union to recover the original language. However, in general, no polynomial-time algorithm is known for computing such decompositions. In this paper, we focus on automata that recognize ideals, that is, languages at level 1/2 in the Straubing-Thérien hierarchy. Equivalently, these languages are expressible as a finite union of languages of the form $Σ^*a_1Σ^*\dotsΣ^*a_nΣ^*$ where $Σ$ is an alphabet and $a_i$ are letters of $Σ$. We show that the two problems of deciding whether such a language can be decomposed into an intersection or a union of smaller automata are decidable in NL. Moreover, we provide a polynomial-time algorithm that computes a decomposition into an intersection, if one exists, while ensuring that the resulting components also recognize ideal languages.

2026-04-28T13:25:05Z Mathias Berry Pierre-Cyrille Héam Ismaël Jecker http://arxiv.org/abs/2606.27867v1 2026-06-26T09:09:28Z

Traditional model-checking techniques typically verify distributed algorithms only for a fixed number of finite-state processes. Parameterized model checking generalizes this to any number of processes, while still typically assuming that each process is finite-state. In this work, we consider asynchronous round-based distributed algorithms in which each process is infinite-state since it can execute for an infinite number of rounds. We show that the parameterized verification problem for asynchronous round-based distributed algorithms is undecidable, already for simple specifications. Nevertheless, as our main contribution, we provide a reduction to LTL model checking over finite-counter systems and prove that it is sound and complete. This enables the use of off-the-shelf, mature symbolic model checkers for finite-counter systems. We demonstrate the practical applicability of this reduction by verifying safety and liveness properties of several asynchronous round-based consensus and leader-election algorithms using the nuXmv model checker.

2026-06-26T09:09:28Z Nathalie Bertrand Pranav Ghorpade Sasha Rubin http://arxiv.org/abs/2408.12240v7 2026-06-26T08:21:55Z

Timed automata (TAs) are an extension of finite automata that can measure and react to the passage of time, providing the ability to handle real-time constraints using clocks. In 2009, Franck Cassez showed that the timed opacity problem, where an attacker can observe some actions with their timestamps and attempts to deduce information, is undecidable for TAs. Moreover, he showed that the undecidability holds even for subclasses such as event-recording automata. In this article, we consider the same definition of opacity, by restricting either the system or the attacker. Our first contribution is to prove the inter-reducibility of two variants of opacity: full opacity (for which the observations should be the same regardless of the visit of a private location) and weak opacity (for which it suffices that the attacker cannot deduce whether the private location was visited, but for which it is harmless to deduce that it was not visited); we also prove further results including a connection with timed language inclusion. Our second contribution is to study opacity for several subclasses of TAs: with restrictions on the number of clocks, the number of actions, the nature of time, or a new subclass called observable event-recording automata. We show that opacity is mostly decidable in these cases, except for one-action TAs and for one-clock TAs with $ε$-transitions, for which undecidability remains. Our third (and arguably main) contribution is to propose a new definition of opacity in which the number of observations made by the attacker is limited to the first $N$ observations, or to a set of $N$ timestamps after which the attacker observes the first action that follows immediately. This set can be defined either a priori or at runtime; all three versions yield decidability for the whole TA class.

2024-08-22T09:17:59Z Logical Methods in Computer Science, Volume 22, Issue 2 (June 29, 2026) lmcs:16104 Étienne André Sarah Dépernet Engel Lefaucheux 10.46298/lmcs-22(2:31)2026 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