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.

ALT Many network protocols and distributed systems combine recursion, unbounded local state, and quantitative behaviour such as cost, latency, or reliability. Existing decidability results for networks of pushdown systems are largely qualitative, and do not extend to quantitative analyses, which must jointly track traces and weights. We present a framework for the quantitative verification of acyclic networks of weighted pushdown systems. Finitely summarising a recursive network component requires collapsing the infinite family of runs obtained by pumping its nested loops, and doing so exactly, rather than by over-approximation, is a standing difficulty. We give a class of weight domains where this is possible: pumping semirings, those in which the weights accumulated by such a family collapse to a closed form; informally, the domain must be unable to count iterations. The class admits domains with infinite ascending chains, such as the arctic semiring and downward-closed languages. Over t

ALT If the machines of some type A have enough resources to (i) solve problems that no machine of type B can solve, and (ii) simulate any unary two-way deterministic finite automaton that has access to a linearly-bounded counter, then typically no recursive function can upper bound the increase in the size of description when a machine of type A is replaced by an equivalent machine of type B.

ALT We prove that no recursive function can upper bound the increase in the size of description when a two-way deterministic finite automaton with k+1 heads is replaced by an equivalent two-way deterministic finite automaton with k heads. This is true for all k, and remains true if the automata are unary and/or nondeterministic.

ALT Thompson's classical construction turns every regular expression into an equivalent epsilon-NFA whose transition graph is series-parallel. The construction uses epsilon-transitions, and eliminating them by the usual shortcut construction need not preserve planarity or the bound of two on the treewidth of the transition graph. Book and Chandra proved that every regular language nevertheless has an epsilon-free NFA with a planar transition graph. We show that the transition graph can in fact be chosen to be a bipartite cactus: every cycle is even, and any two cycles have at most one vertex in common. In particular, it is outerplanar and has treewidth at most two. This is a considerably more simple structure than the general series-parallel guarantee supplied by Thompson's construction. The proof is a direct induction on parity-typed regular expressions and uses only elementary closure properties of cactus graphs.

ALT We introduce and study pattern-based tree transformations. As an illustrating example, consider a source pattern (x ⋅ y) + (x ⋅ z) and a target pattern x ⋅ (y + z) as a pair. This source pattern matches any expression e of the form (e₁ ⋅ e₂) + (e₁ ⋅ e₃) (by substituting x with e₁, y with e₂, and z with e₃) and the pair transforms it into the expression e₁ ⋅ (e₂ + e₃) as dictated by the target pattern. Note that in this example, the set of expressions that match the source pattern is not a regular tree language. We propose a model of tree transformations given by a finite representation of a (possibly infinite) set of such (source pattern, target pattern) pairs. The expressive power of this model comes at the cost of undecidability of checking equivalence. Nevertheless, we show that the type-checking problem is decidable for our model of pattern-based tree transformations. The type-checking problem asks whether applying a given transformation to trees having a given regular property (ty