ALT Verifying cyber-physical systems with many interacting agents remains difficult because interactions are mediated by sensors, individual decisions are constrained by environment (map) structure, and the resulting mode space scales combinatorially. We present Verse, a framework for writing agents, maps, and sensors in a familiar programming language syntax, with a formal semantics for the resulting scenarios. A compiler translates each scenario to a hybrid automaton whose executions correspond exactly to the runs of the scenario. Reachability analysis on this automaton builds an execution tree from two post operators, one for continuous flow over a time step and one for a single agent's mode change, and checks safety assertions at every vertex. The tree expands only the modes that are reached, without enumerating the global mode space. Experiments highlight expressive modeling across cars and drones, 2D/3D maps (including OpenDRIVE imports), noisy sensors, and multiple simultaneous safe

ALT We give a new checkable criterion to ensure that a one-dimensional cellular automaton on a finite alphabet is locally eventually onto. In this setting, openness is equivalent to being n-to-1 for some n and therefore implies surjectivity. Bipermutive cellular automata are known to be locally eventually onto, while open cellular automata that are neither bipermutive nor bijective appear to have received less attention. Building on Sutner's work with de Bruijn graphs, we describe a method for deciding openness and at the same time determining n. We then introduce the notion of block-regularity of local rules as a generalization of bipermutivity and prove that it implies openness. We further identify two conditions that, together with block-regularity, ensure that every nonempty cylinder set is mapped onto the whole configuration space after a finite number of iterations, and hence that the cellular automaton is locally eventually onto. The appendix provides the algorithms that check these

ALT This paper investigates how the algebraic and analytic properties of ordinary length generating functions constrain the grammatical and computational complexity of formal languages. We review the Chomsky-Schutzenberger representation, DSV translations for unambiguous context-free grammars, and their stack-indexed extensions, distinguishing finite algebraic systems from more general constructions. Examples and a diagonal argument demonstrate that even a rational generating function need not determine a language's grammatical class. Our central computability result establishes that, for a recursively enumerable language, computability of its length-counting sequence is equivalent to decidability of membership. Consequently, if a recursively enumerable language has a D-finite length generating function over Q(z), it is decidable; equivalently, undecidable recursively enumerable languages cannot have D-finite length generating functions. We then examine coefficient growth and singularities

ALT A segmentation policy assigns to each byte string at most one segmentation into tokens. Call it finitely verifiable when a finite automaton over marked strings, bytes paired with boundary bits, accepts exactly the policy's own segmentations. The automaton judges a proposed segmentation and need not compute one. The paper shows what that hypothesis buys. Four questions that practice settles by folklore become decidable, whether a window certifies a token boundary, whether the boundary gap is bounded, whether a mask keeps generation completable, and whether two policies are equivalent. The last three specialize limitedness, coaccessibility and the equivalence of single-valued transducers. The first refines the synchronizing cut of code theory, and two more ask whether a certified cut, or the cuts of an inventory, let each piece scan alone. The class sits strictly between the online-scannable policies and those with regular domains, and its inner frontier is Choffrut's and decidable in po

ALT A semilinear set is stratifiable if it is a finite union of linear sets whose periods have at most two nonzero coordinates, with no two periods in one component connecting alternating pairs of coordinates. We give a computable many-one reduction from the existence of a rational zero of an integer polynomial to deciding stratifiability. After the classical reduction to quadratic systems, we reduce rational solvability of these systems to a problem we call finite separation by Cartesian products of rational linear forms. Its input consists of rational subspaces D₁,…,D_k≤mathbbQ^r×mathbbQ^r. A separator is a map (boldsymbol x,boldsymbol y)mapsto(u(boldsymbol x),v(boldsymbol y)), where u,vcolonmathbbQ^r→mathbbQ are nonzero rational linear forms. The problem asks whether finitely many separators suffice so that every pair outside bigcup_iD_i receives, from some separator, a value attained at no pair in that union. We then reduce this problem to stratifiability. Ginsburg and Spanier's charac

ALT 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 bo

ALT 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.

ALT 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

ALT Active model learning is a crucial technique for automatically constructing formal models of black-box timed systems. However, existing learning approaches typically construct a single monolithic automaton for a timed system with multiple synchronous components, obscuring its component structure and hindering component-level analysis. We propose a compositional learning approach that constructs a deterministic real-time automaton (RTA) for each component with access only to the target system as a whole. Upon termination, the learned RTAs form a network that exhibits exactly the same timed behaviors as the target system. Within the respective resource limits, our implementation terminates successfully on 213 of the 240 (88.8%) randomly generated benchmark instances and all six adapted case-study benchmarks, and requires less learning time than monolithic approaches on some instances.

ALT Greibach and Ginsburg (1969) studied abstract families of languages or AFLs. A full AFL is a class of languages closed under the following operations: homomorphism, inverse homomorphism, intersection with regular languages, union, concatenation, and Kleene star. Greibach (1970) used a restricted substitution, called nested iterated substitution, to introduce the notion of super AFLs, which are full AFLs that are further closed under nested iterated substitution. The smallest super AFL was shown to be the class of all context-free languages. From this fact, we focus on Greibach's limited, univariable application of nested iterated substitution and further generalize it into k-variate. This introduces the notion of nested iterated k-variate substitution whose definition does not rely on "machines". Recently, a "two-tape" version of Hibbard's (1967) rewriting systems, which were later reformulated by Pighizzini and Pisoni (2014) as k-limited automata with "single" input/work tapes, has be

ALT 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.

ALT For every n≥22, we construct a language over a fixed three-letter alphabet whose two-way deterministic state complexity is n and whose complement has state complexity 2n. Acceptance is at the left endmarker, and infinite computations reject. The lower bound holds for arbitrary deterministic recognizers. The proof uses the group of transformations induced by the witness to constrain the behavior of a smaller recognizer, then derives a contradiction from a permutation query problem. A matching halting complement follows from a 2n-state construction for sources whose destination states determine the direction of each transition. Splitting states by incoming direction gives a 2n+2b upper bound for general sources, where b counts states entered in both directions. In the acceptance-anywhere model of Geffert, Mereghetti, and Pighizzini, the same family has exact complexities N and 2N-1 for every N≥23.

ALT Jumbled scattered factors are a generalisation of scattered factors (or subsequences) where a jumbled scattered factor is obtained from another word by deleting and rearranging letters. For limiting the number of rearrangements, we distinguish ℓ-jumbled scattered factors where ℓ limits the number of letters that may occur rearranged. For instance, 𝚌𝚊𝚛, 𝚜𝚝𝚊𝚛𝚝, 𝚛𝚊𝚝, 𝚌𝚊𝚝 are jumbled scattered factors of 𝚊𝚋𝚜𝚝𝚛𝚊𝚌𝚝 even though 𝚌𝚊𝚛, 𝚜𝚝𝚊𝚛𝚝 and 𝚌𝚊𝚝 are no scattered factors and each need one jumble. An example for a jumbled scattered factor with 2 jumbles is 𝚝𝚊𝚝𝚊𝚛. In this work, we investigate two problems on jumbled scattered factors from an algorithmic perspective. First, we give algorithms for testing jumbled Simon's equivalence where two words are equivalent if they share the same ℓ-jumbled scattered factors up to length k. Second, we investigate how to count the possible occurrences of a jumbled scattered factor – the jumbled binomial coefficient. After

ALT We study a formulation of regular language membership as a promise problem, which we dub conditional membership: we fix a promise language P and a target language T ⊆ P, we are given a word w which is promised to belong to P, and we must determine whether w belongs to T. We study the deterministic worst-case query complexity of this task, when the length n of w is known in advance and where each query examines the i-th position of w for some 1 ≤ i ≤ n and returns the i-th letter wᵢ of w. Our goal is to characterize the asymptotic complexity as a function of the word length n, depending on the fixed languages P and T. Our main result is to show that the complexity of this task admits a trichotomy between three regimes: O(1) queries, Θ(log n) queries, and Θ(n) queries. We further show that the trichotomy criterion is decidable, namely, it is PSPACE-complete to decide which regime applies, given nondeterministic automata A_P and A_T respectively representing P and T.

ALT Using the formalism of presheaf automata, we introduce new classes of automata for modelling concurrency that extend higher-dimensional automata and symmetric higher-dimensional automata. We study their languages and characterise these languages in terms of posetal cospans.

ALT 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.

ALT In 2022 Dassow and Jecker started investigations on the operational complexity of the pumping constant w.r.t. two pumping lemmata. Since then, the research on pumping lemmata emerged to several variants for regular as well as context-free languages. Within this work, we further investigate the witnesses of regular languages (firstly introduced by Rauch) w.r.t. different pumping lemmata: For a language L and a minimal pumping constant K, a witness of a language is a word that cannot be pumped by K w.r.t. the given pumping lemma. Here, the pumping constant is minimal if for all smaller numbers, the pumping lemma condition is not satisfied. Alongside combinatorial investigations on (unary) witness languages, we introduce and study the measure of scattered factor distance, which is related to minimal pumping constants. We present bounds on minimal pumping constants by the scattered factor distance and show that deciding, given two regular languages, whether one of them is equal to the witn

ALT Rabin games have their roots in Michael Rabin's seminal work on automata over infinite trees and form a classical model for infinite-round games with ω-regular winning conditions. They play a central role in automata theory and temporal synthesis: translating an LTL specification into an equivalent deterministic Rabin automaton reduces synthesis to solving a Rabin game. In practice, however, Rabin games are typically solved indirectly, via parity games. One possible reason is that many direct algorithms have a factorial dependence on the Rabin index k, the number of Rabin pairs. In this work, we revisit Rabin's 1972 recursive algorithm. The algorithm is implicit in Rabin's proof and intertwined with finite-state determinacy. First, we "excavate" it as an explicit arena-based solver using standard reachability- and Büchi-game solving as basic building blocks, thus avoiding the exponential dependence on the alphabet in Rabin's original presentation. Second, we show that memoization rem

ALT We present asymptotically optimal translations from linear temporal logic with past to limit-deterministic Buchi automata and onwards to deterministic parity automata. In contrast to previously known translations involving past, the ones presented here are incremental: states and transitions can be constructed as needed on-the-fly, and they do not involve backtracking in order to correct for temporal inconsistencies. The past is naturally encoded in the formula by alternating between weak and strong versions of past operators. To handle the difficulties that arise from the alternation of least and greatest fix-point operators (such as between the "until" operator and its weak counterpart), we rewrite the given formula based on the infinitary behavior of a given word with respect to subformulae rooted with such operators.

ALT We classify prime accessible deterministic automata over finite alphabets, both among finite automata and among automata with arbitrary state sets. Every one-state automaton is prime. Over a one-letter alphabet, a finite nontrivial automaton is prime exactly when it is a cycle of prime-power length or a finite chain ending in a fixed state. The unique infinite accessible unary automaton, up to isomorphism, is also prime. Every nontrivial automaton over an alphabet with at least two letters is not prime. Shen proved the finite case; we give a shorter proof. We also characterize a decomposition of the automaton whose states are all finite input words. The reachable product of the quotients by the least right congruences identifying the empty word with nonempty words p and q, respectively, is isomorphic to this automaton exactly when pʳ≠ qˢ for all positive integers r,s.