6,133 papers in this slice of arXiv.
Andy Yang, Blerta Veseli, Corentin Barloy +5
Transformer-based language models are known to sometimes generalize to sequences longer than seen during training, but we lack a precise characterization of which tasks admit length generalization. It is not even known which regular languages transformers length-generalize on -- and this is a foundational class of languages. Our contributions are to establish the first complete characterization of which regular languages transformers length-generalize on and provide a decision algorithm running in polynomial time in the size of the language's syntactic monoid. These results rely on an effective characterization of the regular languages in C-RASP, a recently-established formalism that expresses which languages transformers length-generalize on. This characterization is challenging because classical tools like Krohn-Rhodes decomposition theory for finite semigroups are insufficient for C-RASP. Firstly, the basic building blocks of Krohn-Rhodes theory -- flip-flop and simple groups -- are not expressible in C-RASP. Secondly, the basic building block of C-RASP (unbounded counting) is not expressible by the finite semigroups of Krohn-Rhodes theory. Thus, length generalization on regular languages is controlled by an algebraic property that is invisible to classical finite decomposition theory. We generalize classical decomposition theory from finite semigroups to the infinite additive group on the integers, allowing us to characterize C-RASP in terms of iterated wreath products of the integers and derive a provable polynomial-time decision algorithm for regular language membership. Experiments across a broad test suite of regular languages confirm that our theory captures transformers' length-generalization behavior more accurately than existing classifications.
Logan Kenwright, Partha Roop, Sobhan Chatterjee +1
Signal Temporal Logic (STL) is a popular formalism for the temporal safety properties of cyber-physical systems, most often used for runtime verification. In the synchronous family of languages, safety properties are instead expressed as synchronous observers, modules composed with a program for static verification, which are also runnable specifications suitable for runtime verification, though this use is rarely explored. We present a technique for compiling the synchronous fragment of STL (SSTL) into synchronous observers in the dataflow language Lustre. Unlike previous work, we allow arbitrary nesting of bounded SSTL properties via modular compilation, and admit a globally unbounded outer operator for online monitoring; the resulting observers serve both runtime verification and, as a by-product, static verification with the Kind2 model checker. We further contribute an interactive visualiser that renders a property's three-valued verdict over an editable trace, and evaluate on two case studies from the literature: a spring-mass system and a car-following cruise controller.
Xingzi Xu, Karim Bouyarmane
Large language models increasingly need to generate structured outputs that conform to predefined schemas, with one common constraint being selection from a finite set of valid strings. Current constrained decoding systems handle this through general-purpose grammar compilation, which becomes prohibitively slow as the number of valid values grows into the thousands, a cardinality wall. We introduce the trie automaton, a specialized mechanism that exploits finite-set structure (shared prefixes, bounded depth, known cardinality) via Aho-Corasick multi-pattern matching to precompute per-node token masks. The trie achieves 7X faster per-step valid-token computation (0.65 us vs. 5.8 us) compared to XGrammar, one of the primary backends in vLLM and SGLang, and 2--6.5X faster compilation at K >= 300. Because precomputed masks enable a stateless serving path that bypasses the guided decoding pipeline, this advantage compounds in batch serving: end-to-end vLLM throughput reaches 219 req/s vs. XGrammar's 7.5 req/s at batch size 256 (29X). The 29X combines the algorithmic speedup with integration-path savings that only precomputed masks can unlock. Across seven tokenizer families (32K--262K vocabulary), the trie maintains sub-100ms compilation up to K = 10,000 and flat per-step cost regardless of set size, while guaranteeing 100% output validity.
Selim Jerad, Anej Svete, Jiaoda Li +1
Two accounts recur in explanations of the success of rotary position embeddings (RoPE). Expressivity studies associate periodic position information with modular predicates, whereas mechanistic and long-context studies emphasize positional anchors and local offsets. We formalize both accounts for fully uniform, finite-precision soft-attention transformers. We find that, if every rotary component is periodic, RoPE transformers recognize exactly the languages definable in past temporal logic with modular predicates. Conventional RoPE is different: The rotations it computes never repeat. This yields a precision-dependent bounded simulation of fixed-offset look-back operators, rather than an all-length modular characterization. Controlled experiments match this separation: Constructed periodic schedules length-generalize on modular languages, while conventional RoPE behaves more like a bounded locality bias and can impair tasks requiring position-invariant access to distant context. Altogether, our findings shed light on RoPE transformers, bringing theoretical expressivity characterizations closer to models used in practice.
Marius Bozga, Radu Iosif, Florian Zuleger
Triangle graphs are graphs of tree-width at most three in which every edge belongs to a triangle. This class encompasses well-known graph families such as Apollonian networks. We also consider fan graphs, a subclass of triangle graphs closely related to the 3-connected triangle graphs. Our main result is an algebraic characterization of both classes. We introduce two graph algebras based on parallel composition and a ternary serial composition, and show that they generate exactly the triangle and fan graphs, respectively. These algebras provide a natural extension of the classical algebra of series-parallel graphs from tree-width two to tree-width three. Building on these characterizations, we investigate context-free, recognizable, and logically-definable graph languages. We show that counting monadic second-order logic (CMSO) is decidable over the context-free sets of triangle and fan graphs. Moreover, we prove that recognizable graph languages coincide with languages definable in CMSO for both algebras.
Stefan Göller, Paweł Parys
We consider the problem of deciding whether a given pushdown system all of whose ε-transitions are deterministic is weakly bisimulation finite, that is, whether it is weakly bisimulation equivalent to a finite system. We prove that this problem is 2-ExpTime-complete. This consists of three elements: First, we prove that the smallest finite system that is weakly bisimulation equivalent to a fixed pushdown system, if exists, has size at most doubly exponential in the description size of the pushdown system. Second, we propose a fast algorithm deciding whether a given pushdown system is weakly bisimulation equivalent to a finite system of a given size. Third, we prove 2-ExpTime-hardness of the problem. The problem was known to be decidable, but the previous algorithm had Ackermannian complexity (6-ExpSpace in the easier case of pushdown systems without ε-transitions); concerning lower bounds, only ExpTime-hardness was known.
Zhiming Chi, Lutan Zhao, Depeng Liu +8
Branch predictors improve instruction-level parallelism in modern processors and are commonly modeled using saturating counters. However, classical saturating counters are deterministic and thus vulnerable to side-channel attacks: an attacker can manipulate the counter state and infer the branch direction of a victim process. Probabilistic saturating counters (PSCs) have been proposed to mitigate this leakage by randomizing counter updates, but existing evaluations are mainly empirical. In this paper, we give a formal analysis based on differential privacy (DP): we model PSCs and the corresponding Prime+Probe attack strategies as probabilistic Moore machines, derive optimal attack strategies, and quantify the attacker's distinguishing power through DP. Our DP guarantee applies to the PSC primitive under the Prime+Probe observation model; end-to-end security for a full branch predictor under repeated or adaptive attacks is an important direction for future work. We then synthesize parameters for an enhanced PSC that satisfies a target pure DP guarantee. To evaluate utility, we derive the stationary misprediction rate and validate the theoretical predictions on benchmark programs. Compared to deterministic and existing probabilistic saturating counters, the synthesized PSCs provide formal security guarantees while preserving competitive prediction performance.
André Carvalho, Ana-Catarina C. Monteiro
We initiate the study of conjugacy languages in free inverse monoids. Motivated by the notion of conjugacy languages in groups and the study of conjugacy in semigroups, we introduce the language of shortest representatives of conjugacy classes and study it for free inverse monoids of rank at least 2 under the natural notion of conjugacy. We show that, contrary to the free group case, where this language is regular, in a free inverse monoid it is neither context-free nor co-context-free. In the monogenic case, this language is context-free. We show that this non-context-freeness comes from elements with nontrivial conjugacy classes. We define an equivalence relation as follows: all elements with a nontrivial conjugacy class are related and elements with trivial conjugacy class are only related to themselves. We call this relation UConj. We show that the language consisting of geodesics representing elements whose conjugacy class is trivial is context-free by providing an explicit context-free grammar generating it. For groups, we show that the language of minimal representatives of UConj classes is regular if the group is hyperbolic and for right-angled Artin groups with the standard generating set, it is piecewise testable. For virtually abelian groups, we show that there is a generating set for which this language is piecewise excluding and exhibit an example of a virtually abelian group admitting a generating set for which this language is not regular.
Nicklas Nidhögg
A certified split point lets a parallel lexer cut unlexed input at a single byte with the serial token stream provably preserved, but several conventional token sets in the predecessor's controlled study certify no byte once string, comment, or whitespace-run forms are included (arXiv:2608.03473). We generalize from a byte to a bounded window: a byte string after which the position where the current token began is known, regardless of surrounding context. We certify the directly usable form of that recovery: the token covering the window's final byte begins at the reported origin. The certificate is conditional on occurrence and may be vacuous; every applicability figure counts only windows carrying an asserted completely tokenizable occurrence witness. We give a conservative model of a maximal-munch scanner's possible histories across a window, prove it sound, and decide reachability in that model exactly by exhausting a finite quotient of its reachable configurations, so every answer of the unbudgeted procedure is either a certified window with its origin or a proof that the model admits none. Within the stated flat, non-nullable, completely-tokenizable scope, model-positive answers are semantic certificates; negatives are relative to the conservative model, which deliberately refuses some windows a greedy scanner would allow. In a sample of 400 random token sets, 91 of the 95 non-nullable sets certifying no byte gain a witnessed window, with zero inconclusive searches, and every exact-empty row of the predecessor's study gains a witnessed window of two to four bytes. Rewind-stress rows exercised 1,079,392 executions that scanned through the window and contained at least one rewind, with zero disagreements against the shipped scanner. The analysis runs once after automaton construction, using only the compiled tables and no input.
Negin Ayoughi, Baharin A. Jodat, Armina Faghihi +3
Inferring behavioural models from system executions is essential for supporting formal verification and analysis of complex, heterogeneous cyber-physical systems (CPS). Automata learning provides an effective way to infer state machine models from system executions. However, CPS inputs and outputs often consist of numeric time-series data, while automata learning algorithms assume inputs over a finite symbolic alphabet. As a result, raw numeric data must first be abstracted into a finite set of symbols. In this article, we present MELA, a passive automata learning approach enhanced with machine learning to synthesize behavioural models from numeric time-series data generated by CPS. MELA systematically combines statistical machine learning with automata learning to automatically abstract raw numeric signals into interpretable intervals that are strongly correlated with system states. Specifically, MELA uses information-theoretic variable selection and decision-tree-based range abstraction to transform numeric traces into symbolic representations suitable for automata learning. We evaluate MELA on two CPS: a commercial network intrusion detection system developed by our industry partner, RabbitRun Technologies, and a publicly available industrial autopilot benchmark from the aerospace domain. Compared with expertise-based numeric data abstraction, MELA reduces the number of states and transitions in the learned state machines by 49.20% on average, while improving accuracy by 41.71% on average. Furthermore, the learned state machines support system-level requirement verification and help practitioners explore behaviours that are not explicit in the system requirements. We make our implementation and experimental data available online. Keywords: Automata learning, Cyber-physical systems, Behavioural model synthesis, Decision trees, Model checking, Intrusion detection, Simulink.
Sam Nicholas Kouteili, William Fishell, Mark Santolucito +1
Constrained specification mining enables the automatic discovery of desired properties from system traces. Generalized Reactivity of Rank 1, or GR(1), is a fragment of LTL with polynomial-time synthesis that natively encodes assume-guarantee properties present in most hardware and robotics domains. In this paper, we present GR1MINE, a SAT-based tool for efficiently learning GR(1) formulas from examples. We exploit the GR(1) temporal skeleton to incrementally enumerate formula candidates, leveraging learnt clauses to avoid recomputation. On the Boolean GR(1) Syntech suite, GR1MINE learns a realizable formula for all 60 benchmarks over 30X faster than generic and constrained LTL mining tools. On non-GR(1) specifications from SYNTCOMP, GR1MINE is still able to recover >2X more realizable specifications than baselines within the timeout.
Stefanie Muroya, Krishnendu Chatterjee, Thomas A. Henzinger
While most research on quantum programming considers an idealized, noise-free semantics for quantum programs, we reason about quantum programs that are executed on real, noisy hardware. We consider the error models published by quantum hardware vendors to give a hardware-dependent semantics to quantum programs. This work presents a comprehensive study of noise-aware quantum programming, ranging from logical foundations to automated verification and synthesis. We develop a noise-aware quantum Hoare logic, and use it to derive algorithmic methods for the bounded verification of quantum programs on specific hardware, and for the automatic synthesis of noise-optimal loop-free quantum programs. In this way, we synthesize hardware-dependent subroutines that commonly occur in quantum algorithms, such as parity checks, quantum state preparation, and quantum state discrimination. We evaluate our method on the hardware specifications provided by the IBM Qiskit toolkit. Besides finding different optimal subroutines for different noise models, our synthesis tool also shows that classical probabilistic branching is needed for optimality in quantum programming.
Zetong Xuan, Yu Wang
This work studies model-free reinforcement learning for co-safe linear temporal logic (sc-LTL) objectives in finite Markov decision processes, which can be reduced to maximal reachability objectives via the standard product construction. For this problem, direct sample-based bootstrap methods (e.g., TD or Q-learning) may fail to converge to optimal policies due to the noncontractive nature and nonuniqueness of solutions to the Bellman equation. We develop a new two-step model-free reinforcement learning method that first uses a discounted surrogate to identify a clamp set that resolves this nonuniqueness, and then applies undiscounted policy evaluation and greedy policy improvement with guarantees of finding an optimal solution. We prove almost-sure convergence of the policy evaluation step and finite termination of the policy iteration algorithm at an optimal policy. These theoretical results are validated through numerical experiments on a stochastic grid world.
Nicklas Nidhögg
Table-driven DFA lexing is sequential: each transition depends on the previous byte's state. Scanning one input in parallel needs each chunk's entry state, which existing methods recover by simulation, speculation, prescanning, or overlap. We give two conditions under which none is needed. For a longest-match scanner restarting from q0 at every token boundary, a byte b is a certified split symbol when no reachable state other than q0 has a b-transition whose target can reach acceptance, and q0 is not re-entrant if it has one. Every occurrence of such a byte in completely tokenizable input begins a token, so chunks starting there reproduce the serial sequence of kinds and lengths by ordered concatenation. The condition is necessary as well as sufficient, and fragile: one string, comment, or whitespace run can eliminate every useful certificate, and comments and whitespace are usually discarded. We therefore weaken the guarantee to equality after deleting a declared discarded set, and give a second condition, sound and strictly more permissive but conservative rather than exact, decided from the same tables, answered by a second constant-time one-bit query. It recovers newline for a conventional C-like tokenization and tab, newline and carriage return for JSON, without altering their token definitions, and refuses it where block comments are unrestricted. It ships as a query only: the library's planner and every measurement here use the exact condition, so a caller must plan boundaries itself. Splitting at exact certificates in the munch library reaches 92.6-95.3% parallel efficiency at eight threads on a restricted CPU set, on a 512 MiB dense corpus beyond last-level cache, and a 3.46-3.94x end-to-end speedup at four threads, across two benchmark revisions on one machine. It turns delimiter-based parallel lexing from a language-specific assumption into a property a compiler checks.
Raja O. P. Damanik, Alwen Tiu
The intruder deduction problem is central to symbolic security-protocol analysis: it asks whether an attacker can derive a target message from observed messages using (cryptographic) operators available to the attacker. Although convergent rewrite systems provide canonical normal forms, deduction modulo convergent theories remains undecidable in general, and existing decidable fragments are often shaped by practical cryptographic examples. In this paper, we study deduction from a minimal structural perspective. When all function symbols are unary, terms collapse to words and deduction becomes a right-divisibility problem for semi-Thue systems: given words u and v decide whether there exists w such that wu≡Sv. We investigate this problem for several classes of semi-Thue systems and prove, to the best of our knowledge, new decidability results for convergent prefix-erasing and convergent suffix-erasing systems. We then extend this perspective to term rewriting systems whose rules erase contexts while lifting selected subterms or variables. Although these classes suggest possible decidable generalisations beyond the unary setting, we show that deduction is already undecidable for a convergent simultaneous variable-lifting system. This exposes both the potential and the limits of extending the right-divisibility results to richer equational theories.
Akimasa Morihata
Most of the conventional implementations of regular expressions are based on backtracking. Such implementations are slow in the worst case, and thus, we would like to develop a better matching algorithm. However, it is nontrivial to provide an efficient matching algorithm that can deal with practical extensions including submatch addressing. This paper studies regular expression with lookaheads and negative lookaheads, abbreviated to REwLA. First, we propose a transformation from a REwLA of size m to a deterministic finite automaton of O(2²^m) states. Next, we consider weighted regular expressions, which enable us to calculate submatch addressing. We propose a transformation from a weighted REwLA of size m to a weighted nondeterministic finite automaton of O(2²^m) states.
Christoph Weinhuber, Maximilian Prokop, Giuseppe De Giacomo +1
Linear Temporal Logic (LTL) is one of the most widely adopted languages for specifying temporal extended objectives in AI, with applications ranging from reactive synthesis to stochastic planning in Markov decision processes and reinforcement learning. Traditionally, solving any of these problems requires translating the LTL specification to a nondeterministic automata on infinite words and then determinizing it, a step that is notoriously difficult in theory and in practice. Recent work has introduced LTLf+, which lifts the finite-trace logic LTLf to infinite traces. LTLf+ has the same expressive power as LTL, yet it retains most of the crucial advantages of its base logic LTLf. Most reasoning in LTLf+ rests on finite automata on finite words, for which we have not only a canonical minimal representation but also an efficient determinization procedure. In this work we present the first translation from LTL to LTLf+. We first normalize an LTL formula into the syntactic reactivity fragment of the Manna-Pnueli hierarchy, to create the general fragment-based shape of LTLf+. We then present linear translations for each individual component of that fragment. As a consequence of this translation, the expanding body of techniques developed for LTLf+ now becomes available to many AI problems currently formulated in LTL. We further show that this comes at no asymptotic cost, as the pipeline from LTL to automaton via LTLf+ remains doubly exponential.
Zhiming Chi, Ying Liu, Andrea Turrini +2
In this paper, we consider the parameter synthesis and optimization problem for parametric Markov decision processes (pMDPs), the extension of classical MDPs where exact probability values are replaced by parametric expressions. Computing the rational function f_ that maps parameter valuations to the satisfaction value of a PRCTL property is a computationally expensive task, particularly for pMDPs where the optimal policy may vary across the parameter space. We adopt the scenario approach to efficiently synthesize a probably approximately correct (PAC) approximation f of f_: by sampling parameter configurations and solving a linear program, we obtain a polynomial approximation whose error margin is guaranteed, with prescribed confidence, for all but an -fraction of the parameter domain under the sampling distribution. We further show how this PAC framework can be combined with statistical model checking (SMC), enabling the analysis of black-box parametric models. Building on the PAC approximation, we integrate the DIRECT (DIviding RECTangles) algorithm for derivative-free global optimization over the parameter space. We establish conditional optimality-gap guarantees: under explicit Lipschitz and PAC-good-set assumptions, the difference between the true optimum f_(^*) and the value found by DIRECT is bounded by a partition-diameter term and, in the PAC case, an additional approximation-error term. An empirical evaluation on 2997 benchmarks focuses on the new DIRECT-based optimization component. The results show that DIRECT variants solve fewer instances than the scenario optimizer, but on their common successful instances they often return slightly better objective values and usually run faster, while remaining close to the scenario values within the PAC margin.
Corentin Bodart, Daniele D'Angeli, Davide Perego +1
We prove a graph-theoretical characterisation of finitely generated subgroups of Thompson's group V: a finitely generated group embeds in V if and only if it admits a faithful context-free action, or equivalently if it belongs to the class CF-TR of transition groups of context-free graphs recently introduced by Matucci and the three last authors. Using this characterisation, we prove results in different directions: - All known examples of groups with co-context-free Word Problem do embed in V, providing evidence towards Lehnert's conjecture. - Each finitely generated subgroup of V is either virtually abelian, or contains a free non-abelian semigroup. It follows that groups of intermediate growth do not embed in Thompson's V. We further study the relation between transition groups defined by graphs that are limits or covers of each others, and prove properties of transition groups of context-free graphs of polynomial growth. Finally, we prove that the Basilica and Hanoï Towers groups do not embed in V. This uses the geometry of Schreier graphs of the natural actions of these groups and of Thompson's V.
Sergey Salishev
We study transcript management for fixed, finite-precision causal Transformers. A transcript is partitioned into channels of bounded blocks. Each transition consults a fixed visible suffix and may append one block, leaving the model, weights, and token protocol unchanged. The operation P_c:=(c) deletes the newest block on channel c and exposes its predecessor. We model the layer by the Transcript-Managed Transducer k: one finite controller, k channels, and per-round actions from stay, push, and pop under a caller-driven status map. Fixed visible windows encode as finite symbols. The pop-free Restricted Transcript-Managed Transducer k is the standard append-only layer and, for every fixed k, realizes exactly the deterministic finite-state transductions. The same holds for every fixed finite agent population under a monotone protocol that appends, routes, and copies visible blocks. Admitting {Pc}c=1k restores pop. Newest-first, a pop-enabled channel is a stack; compiling to the Hopcroft--Ullman presentation transfers the classical hierarchy: for k=1 and for every k≥2. Orchestrated one-channel agents match one controller with k channels, so two pop-enabled transcripts---in one agent or two---suffice for universality. Simulation costs and invariance to fixed block size and visible radius are stated. The bounds fix precision, alphabets, blocks, visibility, controller state, and population; growing exact context, hidden-block access, writable stores, and unbounded Spawn add further state.