https://arxiv.org/api/QmWNa5OFXHdbm/WJhQ+R8dF8x/U2026-03-28T12:56:40Z587915015http://arxiv.org/abs/2602.02698v1Compiling Quantum Regular Language States2026-02-02T19:11:38ZState preparation compilers for quantum computers typically sit at two extremes: general-purpose routines that treat the target as an opaque amplitude vector, and bespoke constructions for a handful of well-known state families. We ask whether a compiler can instead accept simple, structure-aware specifications while providing predictable resource guarantees. We answer this by designing and implementing a quantum state-preparation compiler for regular language states (RLS): uniform superpositions over bitstrings accepted by a regular description, and their complements. Users describe the target state via (i) a finite set of bitstrings, (ii) a regular expression, or (iii) a deterministic finite automaton (DFA), optionally with a complement flag. By translating the input to a DFA, minimizing it, and mapping it to an optimal matrix product state (MPS), the compiler obtains an intermediate representation (IR) that exposes and compresses hidden structure. The efficient DFA representation and minimization offloads expensive linear algebra computation in exchange of simpler automata manipulations. The combination of the regular-language frontend and this IR gives concise specifications not only for RLS but also for their complements that might otherwise require exponentially large state descriptions. This enables state preparation of an RLS or its complement with the same asymptotic resources and compile time. We outline two hardware-aware backends: SeqRLSP, which yields linear-depth, ancilla-free circuits for linear nearest-neighbor architectures via sequential generation, and TreeRLSP, which achieves logarithmic depth on all-to-all connectivity via a tree tensor network. We prove depth and gate-count bounds scaling with the system size and the state's maximal Schmidt rank, and we give explicit compile-time bounds that expose the benefit of our approach. We implement and evaluate the pipeline.2026-02-02T19:11:38ZCode available at https://github.com/reinisirmejs/RLSCompArmando BellanteReinis IrmejsMarta Florido-LlinàsMaría Cea FernándezMarianna CrupiMatthew KiserJ. Ignacio Cirachttp://arxiv.org/abs/2602.02447v1Deciding Reachability and the Covering Problem with Diagnostics for Sound Acyclic Free-Choice Workflow Nets2026-02-02T18:41:58ZA central decision problem in Petri net theory is reachability asking whether a given marking can be reached from the initial marking. Related is the covering problem (or sub-marking reachbility), which decides whether there is a reachable marking covering at least the tokens in the given marking. For live and bounded free-choice nets as well as for sound free-choice workflow nets, both problems are polynomial in their computational complexity. This paper refines this complexity for the class of sound acyclic free-choice workflow nets to a quadratic polynomial, more specifically to $O(P^2 + T^2)$. Furthermore, this paper shows the feasibility of accurately explaining why a given marking is or is not reachable. This can be achieved by three new concepts: admissibility, maximum admissibility, and diverging transitions. Admissibility requires that all places in a given marking are pairwise concurrent. Maximum admissibility states that adding a marked place to an admissible marking would make it inadmissible. A diverging transition is a transition which originally "produces" the concurrent tokens that lead to a given marking. In this paper, we provide algorithms for all these concepts and explain their computation in detail by basing them on the concepts of concurrency and post-dominance frontiers - a well known concept from compiler construction. In doing this, we present straight-forward implementations for solving (sub-marking) reachability.2026-02-02T18:41:58Z38 pages, 18 figuresThomas M. PrinzChristopher T. SchwanenWil M. P. van der Aalsthttp://arxiv.org/abs/2602.02352v1Well-Formed Free-Choice Petri Nets Revisited2026-02-02T17:16:43ZThe theory of free-choice Petri nets is an established field, initiated in the 1970s by Commoner and Hack at MIT. We revisit well-formed free-choice nets (those admitting markings that are both live and bounded) and provide a new characterization by introducing semi-T-components. This notion is dual to that of semi-S-components, which in turn correspond to the well-known minimal siphons. By highlighting the symmetry between these dual concepts, we derive the classical coverability theorems for T- and S-components, as well as the duality theorem -- stating that a free-choice net is well-formed if and only if its reverse-dual is also well-formed -- using arguments that are as symmetric as possible.2026-02-02T17:16:43ZPetr JancarEike BestRaymond DevillersMatej Ostadalhttp://arxiv.org/abs/2209.10517v17On Probabilistic $ω$-Pushdown Systems, and $ω$-Probabilistic Computational Tree Logic2026-02-01T18:40:39ZIn this paper, we define the notion of {\em probabilistic $ω$-pushdown automaton} and study its model-checking problem against the logic of $ω$-probabilistic computational tree logic ($ω$-PCTL) and its bounded version from a computational complexity view. Specifically, we obtain the following equally important new results:
We define {\em probabilistic $ω$-pushdown automaton} for the first time and study the model-checking question of {\em stateless probabilistic $ω$-pushdown system ($ω$-pBPA)} against $ω$-PCTL (defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}), showing that model-checking of {\em stateless probabilistic $ω$-pushdown systems ($ω$-pBPA)} against $ω$-PCTL is generally undecidable. Our approach is to construct $ω$-PCTL formulas encoding the {\em Post Correspondence Problem}.
We then study in which case there exists an algorithm for model-checking {\it stateless probabilistic $ω$-pushdown systems} and show that the problem of model-checking {\it stateless probabilistic $ω$-pushdown systems} against $ω$-{\it bounded probabilistic computational tree logic} ($ω$-bPCTL) is decidable, and further show that this problem is $\mathit{NP}$-hard.2022-09-21T17:33:48Z[v17] Abstract and introduction enriched (with main conclusions unchanged). arXiv admin note: text overlap with arXiv:1405.4806Deren LinTianrong Linhttp://arxiv.org/abs/2602.01221v1A Complexity Bound for Determinisation of Min-Plus Weighted Automata2026-02-01T13:25:07ZThe determinisation problem for min-plus (tropical) weighted automata was recently shown to be decidable. However, the proof is purely existential, relying on several non-constructive arguments. Our contribution in this work is twofold: first, we present the first complexity bound for this problem, placing it in the Fast-growing hierarchy. Second, our techniques introduce a versatile framework to analyse runs of weighted automata in a constructive manner. In particular, this significantly simplifies the previous decidability argument and provides a tighter analysis, thus serving as a critical step towards a tight complexity bound.2026-02-01T13:25:07ZShaull AlmagorGuy ArbelSarai Sheinvaldhttp://arxiv.org/abs/2510.27049v3Recursive numeral systems are highly regular and easy to process2026-01-31T02:56:39ZMuch recent work has shown how cross-linguistic variation is constrained by competing pressures from efficient communication. However, little attention has been paid to the role of the systematicity of forms (regularity), a key property of natural language. Here, we demonstrate the importance of regularity in explaining the shape of linguistic systems by looking at recursive numeral systems. Previous work has argued that these systems optimise the trade-off between lexicon size and average morphosyntatic complexity (Denić and Szymanik, 2024). However, showing that only natural-language-like systems optimise this trade-off has proven elusive, and existing solutions rely on ad-hoc constraints to rule out unnatural systems (Yang and Regier, 2025). Drawing on the Minimum Description Length (MDL) approach, we argue that recursive numeral systems are better viewed as efficient with regard to their regularity and processing complexity. We show that our MDL-based measures of regularity and processing complexity better capture the key differences between attested, natural systems and theoretically possible ones, including "optimal" recursive numeral systems from previous work, and that the ad-hoc constraints naturally follow from regularity. Our approach highlights the need to incorporate regularity across sets of forms in studies attempting to measure efficiency in language.2025-10-30T23:34:41ZPonrawee PrasertsomAndrea SilviJennifer CulbertsonMoa JohanssonDevdatt DubhashiKenny Smithhttp://arxiv.org/abs/2601.23156v1Unsupervised Hierarchical Skill Discovery2026-01-30T16:41:13ZWe consider the problem of unsupervised skill segmentation and hierarchical structure discovery in reinforcement learning. While recent approaches have sought to segment trajectories into reusable skills or options, most rely on action labels, rewards, or handcrafted annotations, limiting their applicability. We propose a method that segments unlabelled trajectories into skills and induces a hierarchical structure over them using a grammar-based approach. The resulting hierarchy captures both low-level behaviours and their composition into higher-level skills. We evaluate our approach in high-dimensional, pixel-based environments, including Craftax and the full, unmodified version of Minecraft. Using metrics for skill segmentation, reuse, and hierarchy quality, we find that our method consistently produces more structured and semantically meaningful hierarchies than existing baselines. Furthermore, as a proof of concept for utility, we demonstrate that these discovered hierarchies accelerate and stabilise learning on downstream reinforcement learning tasks.2026-01-30T16:41:13Z24 pages, 34 figures. Appendix by Damion Harvey. Damion Harvey is the primary authorDamion HarveyUniversity of the Witwatersrand, Johannesburg, South AfricaGeraud Nangue TasseUniversity of the Witwatersrand, Johannesburg, South AfricaMachine Intelligence and Neural DiscoveryBranden IngramUniversity of the Witwatersrand, Johannesburg, South AfricaMachine Intelligence and Neural DiscoveryBenjamin RosmanUniversity of the Witwatersrand, Johannesburg, South AfricaMachine Intelligence and Neural DiscoverySteven JamesUniversity of the Witwatersrand, Johannesburg, South AfricaMachine Intelligence and Neural Discoveryhttp://arxiv.org/abs/2601.23130v1Synthesizing Petri Nets from Labelled Petri Nets using Token Trail Regions2026-01-30T16:19:47ZSynthesis automatically generates a process model from a behavioural specification. When the target model is a Petri net, we address synthesis through region theory. Researchers have studied region-based synthesis extensively for state-based specifications, such as transition systems and step-transition systems, as well as for language-based specifications. Accordingly, in literature, region theory is divided into two main branches: state-based regions and language-based regions. Using state-based regions, the behavioural specification is a set of global states and related state-transitions. This representation can express conflicts and the merging of global states naturally. However, it suffers from state explosion and can not express concurrency explicitly. Using language-based regions, the behavioural specification is a set of example runs defined by partially or totally ordered sets of events. This representation can express concurrency and branching naturally. However, it grows rapidly with the number of choices and can not express merging of conflicts. So far, synthesis requires a trade-off between these two approaches. Both region definitions have fundamental limitations, and synthesis therefore always involves a compromise. In this paper, we lift these limitations by introducing a new region theory that covers both state-based and language-based input. We prove that the new definition is a region meta theory that combines both concepts. It uses specifications given as a set of labelled nets, which allow us to express conflicts, concurrency and merging of local states naturally, and synthesizes a Petri net that simulates all labelled nets of the input specification.2026-01-30T16:19:47ZRobin BergenthumJakub Kovářhttp://arxiv.org/abs/2601.10564v5Rewriting Systems on Arbitrary Monoids2026-01-30T13:47:15ZIn this paper, we introduce monoidal rewriting systems (MRS), an abstraction of string rewriting in which reductions are defined over an arbitrary ambient monoid rather than a free monoid of words. This shift is partly motivated by logic: the class of free monoids is not first-order axiomatizable, so "working in the free setting" cannot be treated internally when applying first-order methods to rewriting presentations.
To analyze these systems categorically, we define $\mathbf{NCRS_2}$ as the 2-category of Noetherian Confluent MRS. We then prove the existence of a canonical biadjunction between $\mathbf{NCRS_2}$ and $\mathbf{Mon}$.
Finally, we classify all Noetherian Confluent MRS that present a given fixed monoid. For this, we introduce Generalized Elementary Tietze Transformations (GETTs) and prove that any two presentations of a monoid are connected by a (possibly infinite) sequence of these transformations, yielding a complete characterization of generating systems up to GETT-equivalence.2026-01-15T16:27:17ZEduardo Magalhãeshttp://arxiv.org/abs/2510.23487v2Are Agents Probabilistic Automata? A Trace-Based, Memory-Constrained Theory of Agentic AI2026-01-30T10:33:57ZThis paper studies standard controller architectures for agentic AI and derives automata-theoretic models of their interaction behavior via trace semantics and abstraction. We model an agent implementation as a finite control program augmented with explicit memory primitives (bounded buffers, a call stack, or read/write external memory) and a stochastic policy component (e.g., an LLM) that selects among architecturally permitted actions. Instead of equating the concrete agent with a deterministic acceptor, we treat the agent-environment closed loop as inducing a probability distribution over finite interaction traces. Given an abstraction function $\Abs$ from concrete configurations to a finite abstract state space, we obtain a probabilistic trace language and an abstract probabilistic transition model $M_{\Abs}$ suitable for probabilistic model checking.
Imposing explicit, framework-auditable restrictions on memory access and control flow, we prove that the support of the resulting trace language is regular for bounded-memory controllers, context-free for strict call-return controllers, and recursively enumerable for controllers equipped with unbounded read/write memory. These correspondences allow the reuse of existing verification methods for finite-state and pushdown systems, and they delineate precisely when undecidability barriers arise. The probabilistic semantics leads to quantitative analyses such as: what is the probability of entering an unsafe abstract region, and how can we bound this probability in the presence of environment nondeterminism.2025-10-27T16:22:02ZRoham KoohestaniZiyou LiAnton PodkopaevMaliheh Izadihttp://arxiv.org/abs/2504.14623v2Synthesising Asynchronous Automata from Fair Specifications2026-01-30T07:07:08ZAsynchronous automata are a model of distributed finite state processes synchronising on shared actions. A celebrated result by Zielonka shows how a deterministic asynchronous automaton (AA) can be synthesised, starting from two inputs: a global specification given as a deterministic finite-state automaton (DFA) and a distribution of the alphabet into local alphabets for each process. The DFA to AA translation is particularly complex and has been revisited several times, with no complete prototype tool provided for the full construction. In this work, we revisit this construction on a restricted class of "fair" specifications: a DFA describes a fair specification if in every loop, all processes participate in at least one action, so no process is starved. For fair specifications, we present a new construction to synthesise an AA. Our construction results in an AA where every process has a number of local states that is linear in the number of states of the DFA, and where the only exponential explosion is related to a fairness parameter: the length of the longest word that can be read in the DFA in which not every process participates. We have implemented a prototype tool showing how it can be applied to some examples, in particular, a concrete one: the dining philosophers problem. Finally, we show how this construction can be combined with an existing construction for hierarchical process architectures, in order to relax the fairness assumption. We have implemented a prototype tool showing how it can be applied to some examples, in particular, a concrete one: the dining philosophers problem. Finally, we show how this construction can be combined with an existing construction for hierarchical process architectures, in order to relax the fairness assumption.2025-04-20T14:01:46ZBéatrice BérardBenjamin MonmegeB SrivathsanArnab Surhttp://arxiv.org/abs/2507.11352v2Foundation Models for Logistics: Toward Certifiable, Conversational Planning Interfaces2026-01-30T00:57:27ZLogistics operators, from battlefield coordinators re-routing airlifts ahead of a storm to warehouse managers juggling late trucks, need to make mission-critical decisions. Prevailing methods for logistics planning such as integer programming yield plans that satisfy user-defined logical constraints, assuming an idealized mathematical model of the environment. On the other hand, foundation models lower the intermediate processing barrier by translating natural-language user utterances into executable plans, yet they remain prone to misinterpretations and hallucinations that jeopardize safety and cost. We introduce a Vision-Language Logistics (VLL) agent, built on a neurosymbolic framework that pairs the accessibility of natural-language dialogue with verifiable guarantees on user-objective interpretation. The agent interprets user requests and converts them into structured planning specifications, quantifies the uncertainty of the interpretation, and invokes an interactive clarification loop when the uncertainty exceeds an adaptive threshold. Drawing on a lightweight airlift logistics planning use case as an illustrative case study, we highlight a practical path toward certifiable and user-aligned decision-making for complex logistics. Our lightweight model, fine-tuned on just 100 training samples, surpasses the zero-shot performance of 20x larger models in logistic planning tasks while cutting inference latency by nearly 50%.2025-07-15T14:24:01ZYunhao YangNeel P. BhattChristian EllisSamuel LiAlvaro VelasquezZhangyang WangUfuk Topcuhttp://arxiv.org/abs/2505.08140v5Lost in Transmission: When and Why LLMs Fail to Reason Globally2026-01-30T00:12:35ZDespite their many successes, transformer-based large language models (LLMs) continue to struggle with tasks that require complex reasoning over large parts of their input. We argue that these failures arise due to capacity limits on the accurate flow of information within LLMs. To formalize this issue, we introduce the bounded attention prefix oracle (BAPO) model, a new computational framework that models bandwidth constraints on attention heads, the mechanism for internal communication in LLMs. We show that several important reasoning problems like graph reachability require high communication bandwidth for BAPOs to solve; we call these problems BAPO-hard. Our experiments corroborate our theoretical predictions: GPT-4o, Claude, and Gemini succeed on BAPO-easy tasks and fail even on relatively small BAPO-hard tasks. BAPOs also reveal another benefit of chain of thought (CoT): we prove that breaking down a task using CoT can turn any BAPO-hard problem into a BAPO-easy one. Our results offer principled explanations for key LLM failures and suggest directions for architectures and inference methods that mitigate bandwidth limits.2025-05-13T00:25:23Z39 pages; NeurIPS 2025, spotlightTobias SchnabelKiran TomlinsonAdith SwaminathanJennifer Nevillehttp://arxiv.org/abs/2601.22402v1Bifocal Attention: Harmonizing Geometric and Spectral Positional Embeddings for Algorithmic Generalization2026-01-29T23:16:31ZRotary Positional Embeddings (RoPE) have become the standard for Large Language Models (LLMs) due to their ability to encode relative positions through geometric rotation. However, we identify a significant limitation we term ''Spectral Rigidity'': standard RoPE utilizes a fixed geometric decay ($θ^{-i}$) optimized for local syntactic coherence, which fails to capture the long-range, periodic structures inherent in recursive logic and algorithmic reasoning. This results in a ''Structure Gap'', where models trained on shallow reasoning chains fail to extrapolate to deeper recursive steps. In this work, we introduce Bifocal Attention, an architectural paradigm that decouples positional encoding into two distinct modalities: Geometric Eyes (Standard RoPE) for precise token-level manipulation, and Spectral Eyes (Learnable Harmonic Operators) for tracking long-range recursive depth. We propose a novel training protocol, Spectral Evolution, which initializes positional frequencies as static geometric parameters but allows them to evolve via gradient descent into a harmonic basis optimized for the specific algorithmic topology of the task.2026-01-29T23:16:31ZKanishk Awadhiyahttp://arxiv.org/abs/2601.21862v1Cellular Automaton Reducibility as a Measure of Complexity for Infinite Words2026-01-29T15:31:16ZInfinite words, also known as streams, hold significant interest in computer science and mathematics, raising the natural question of how their complexity should be measured. We introduce cellular automaton reducibility as a measure of stream complexity: σ is at least as complex as τ when there exists a cellular automaton mapping σ to τ. This enables the categorization of streams into degrees of complexity, analogous to Turing degrees in computability theory. We investigate the algebraic properties of the hierarchy that emerges from the partial ordering of degrees, showing that it is not well-founded and not dense, that ultimately periodic streams are ordered by divisibility of their period, that sparse streams are atoms, that maximal streams have maximal subword complexity, and that suprema of sets of streams do not generally exist. We also provide a pseudo-algorithm for classifying streams up to this reducibility.2026-01-29T15:31:16Z34 pages, 5 figuresMarkel ZubiaHerman Geuvers