https://arxiv.org/api/3us2K77bLd7VOKbJwM4ZzyP/vOM 2026-07-20T22:45:36Z 6096 45 15 http://arxiv.org/abs/2607.01856v2 2026-07-05T19:27:57Z

We present an algebraic method for analyzing probabilistic programs with counters and discrete states, Generalized Constant Probability (GCP) programs. We define the operational semantics of GCP in terms of the runs of a type of probabilistic pushdown automata (pPDAs). We characterize the resulting (sub-)probability generating function (pgf) $Δ(z)$ as an algebraic function, representable via the roots of a kernel polynomial associated with the program. Next, we provide algorithms that, leveraging this information, compute under mild algebraic conditions the dominant singularities and the exact radius of convergence of $Δ(z)$, leading to an exact asymptotic expansion and to exponential bounds for its coefficients. Our approach is sound for GCP programs and complete for the single-state subclass.

2026-07-02T08:15:49Z Michele Boreale Luisa Collodi Alessandro Pompa Di Gregorio http://arxiv.org/abs/2606.30820v2 2026-07-05T18:15:16Z

Time Window Temporal Logic (TWTL) is a rich specification language for cyber-physical systems that can compactly express sequential tasks with explicit timing constraints. In this paper, we consider the problem of synthesizing control inputs for discrete-time linear systems subject to TWTL task specifications. Building on the quantitative semantics (robustness) recently introduced for TWTL in [1], we encode the robust satisfaction of a TWTL formula as a set of Mixed-Integer Linear constraints and pose synthesis as a Mixed Integer Linear Program (MILP) that maximizes the robustness degree. We prove that any feasible solution with positive objective value guarantees Boolean satisfaction of the specification. We address two synthesis settings: an \emph{open-loop} formulation that optimizes the full control sequence from the initial state, and a \emph{closed-loop} receding-horizon Model Predictive Controller (MPC) formulation that re-solves the MILP at each step using the current measured state. A key feature of our MPC formulation is a \emph{task-adaptive horizon} that exploits the TWTL Deterministic Finite Automaton (DFA) to determine the active sub-task at each step, limiting the prediction horizon to the remaining window of the current task rather than the full formula horizon, this makes each re-solve significantly cheaper than the initial open-loop solve.

2026-06-29T18:47:16Z Philip Smith Ahmad Ahmad Kevin Leahy http://arxiv.org/abs/2605.07968v2 2026-07-04T10:34:11Z

We define a quantum computational model over infinite words, called Measure-Many Quantum Büchi Automata (MMQBA), which extends Measure-many Quantum Finite automata (MMQFA) to the infinite word setting with Büchi acceptance condition. In MMQBA, the quantum state evolves through unitary transformations followed by repeated projective measurements. An infinite word is accearaq2ppted with respect to a cutpoint p is in (0, 1] if (i) the run visits accepting states infinitely often, (ii) the limiting cumulative acceptance probability is at least p, and (iii) the limiting cumulative rejection lprobability is strictly less than p. We formalize the semantics of MMQBA, establish a language-theoretic characterization showing that MMQBA languages are precisely of the form lim(L(M, p)) for MMQFA M , and develop a decomposition of the non-halting subspace. We prove that MMQBA is closed under union but not under intersection or complementation. On the algorithmic side, we show that the emptiness problem is semi-decidable, while universality, inclusion, equivalence, and membership remain undecidable.

2026-05-08T16:29:52Z Abhisek Midya A Baskar http://arxiv.org/abs/2510.20692v3 2026-07-03T02:33:17Z

Access control policies are reliability-critical configuration artifacts in cloud systems, yet administrators frequently struggle to verify that a policy permits exactly what they intend. This verification gap cannot be remedied by using LLMs to synthesize policies: we find that reasoning and non-reasoning LLMs fluently explain policy behavior but cannot reason about policy semantics with reliability-grade precision, even when the specification is the LLM's own explanation. We formulate this impasse as the Verifiable Synthesis Paradox: the verification gap persists regardless of how the policy was authored. To remedy this, we introduce PolicySummarizer, a neurosymbolic tool that pairs finite-state automata with an LLM-based simplification to generate precise human-readable characterizations of requests allowed by a policy. PolicySummarizer uses model counting to guarantee the fidelity of the generated characterization by rejecting characterizations that fall below a user-configured threshold in favor of the formally derived one. On 546 AWS, 100 Microsoft Azure, and 100 Google Cloud Platform policies, PolicySummarizer achieves a mean similarity score of 0.93 and a 2.7x improvement over an SMT-based baseline. In a user study, PolicySummarizer raised policy-change-review accuracy from 39% to 93% on the hardest sub-task while reducing self-reported mental demand. We release PolicySummarizer as an open-source tool.

2025-10-23T16:06:15Z Accepted to ISSRE 2026. Major revision and retitling of arXiv:2510.20692v1. Refocuses the paper on reliable neurosymbolic access-control policy analysis; updates the PolicySummarizer method, multi-cloud evaluation, and user-study results. 13 pages, 6 figures. Corrected arXiv title metadata to match the accepted ISSRE version. No substantive content changes from the previous version Adarsh Vatsa Bethel Hall William Eiers http://arxiv.org/abs/2606.08127v3 2026-07-02T19:04:11Z

Let ${\bf x} = (a_i)_{i \geq 0}$ be an infinite word over a finite alphabet $Σ$. Let $ρ(n)$ be the factor complexity function for $\bf x$ and ${\rm Pal}(n)$ be the palindrome complexity function for $\bf x$. We give a new relationship between these two quantities; namely, if $\bf x$ is not ultimately periodic, then $$ \lim_{n \rightarrow \infty} {{ {\rm Pal} (n) \log ({\rm Pal} (n) + 1)} \over {ρ(n)}} = 0. $$ Furthermore, we prove that the numerator in this result is essentially optimal.

2026-06-06T12:11:29Z Jeffrey Shallit http://arxiv.org/abs/2607.01858v1 2026-07-02T08:17:52Z

Automata on linear orderings are finite-state automata introduced by Bruyère and Carton as a broad generalization of finite, infinite and transfinite-word automata. In this context, a word is defined as a function from a linear ordering to a finite alphabet. This general definition can make automata on linear orderings difficult to reason about. In this work, we introduce constructible words as an intuitive way of tackling this difficulty. These words can be obtained by a finite number of applications of simple operators and thus admit a finite notation. We show that a rational language of words indexed by scattered (countable and uncountable) linear orderings is characterized by its constructible words. Our proof of this result relies on an interesting theorem of semigroup theory due to Colcombet. We expect this property to be useful in future theoretical developments about automata on scattered linear orderings.

2026-07-02T08:17:52Z Submitted and accepted to MFCS 2026 Thomas Braipson Tom Clara http://arxiv.org/abs/2607.01837v1 2026-07-02T08:01:44Z

We show that any overlap-free morphism is a $k$-power-free morphism for all integers $k\geq 3$.

2026-07-02T08:01:44Z Francis Wlazinski UPJV http://arxiv.org/abs/2607.01704v1 2026-07-02T04:55:03Z

Unordered trees appear in applications where the order among child vertices is insignificant, such as abstract syntax trees and chemical structures. To describe patterns in such trees, we propose unordered term tree patterns, which employ height-constrained variables that restrict trunk length and subtree height. We formalize the pattern matching problem between an unordered term tree pattern and an unordered tree, and present an $O(N \cdot \max\{nD^{3/2}, \mathcal{S}\})$-time algorithm, where $n$ and $N$ are the numbers of vertices in the pattern and tree, $D$ is the maximum vertex degree, and $\mathcal{S}$ is the sum of trunk constraints. Computational results show that the algorithm runs efficiently in practice.

2026-07-02T04:55:03Z 6 pages. Author preprint of a paper presented at ESKM 2025, IIAI-AAI 2025 Shintaro Matsushita Takayoshi Shoudai Yusuke Suzuki http://arxiv.org/abs/2512.22431v6 2026-07-01T23:46:05Z

The proliferation of Large Language Models (LLMs) has catalyzed a shift towards autonomous agents capable of complex reasoning and tool use. However, current agent architectures are frequently constructed using imperative, ad hoc patterns. This results in brittle systems plagued by difficulties in state management, error handling, and concurrency. This paper introduces Monadic Context Engineering (MCE), a novel architectural paradigm leveraging the algebraic structures of Functors, Applicative Functors, and Monads to provide a formal foundation for agent design. MCE treats agent workflows as computational contexts where cross-cutting concerns, such as state propagation, short-circuiting error handling, and asynchronous execution, are managed intrinsically by the algebraic properties of the abstraction. We demonstrate how Monads enable robust sequential composition, how Applicatives provide a principled structure for parallel execution, and crucially, how Monad Transformers allow for the systematic composition of these capabilities. This layered approach enables developers to construct complex, resilient, and efficient AI agents from simple, independently verifiable components. We further extend this framework to describe Meta-Agents, which leverage MCE for generative orchestration, dynamically creating and managing sub-agent workflows through metaprogramming.

2025-12-27T01:52:06Z We found some issues in the categorical foundations of this work, so we respectfully withdraw it Yifan Zhang Yang Yuan Mengdi Wang Andrew Chi-Chih Yao http://arxiv.org/abs/2607.00742v1 2026-07-01T10:24:10Z

Symmetric difference automata (XNFA) are a variant of standard finite automata in which an input word is accepted iff the number of accepting runs is odd. Equivalently, these are weighted automata over the two-element field. We study the fine-grained complexity of the basic decision problems for XNFA: acceptance, emptiness, and equivalence, aiming to optimise the degree of the polynomial in their running-time bounds. Under the assumption of polynomial ambiguity, we provide a randomised reduction of NFA acceptance to XNFA acceptance. For automata of bounded ambiguity (e.g., unambiguous automata), we show that acceptance for both NFA and XNFA can be decided faster than in the general case. Without ambiguity assumptions, we give faster algorithms for the verification of suitable certificates for (non)emptiness and (non)equivalence of XNFA. Several of our results extend to weighted automata over other semirings and fields.

2026-07-01T10:24:10Z Dmitry Chistikov Radosław Piórkowski Neha Rino Brink van der Merwe http://arxiv.org/abs/2606.31974v1 2026-06-30T17:15:26Z

A two-dimensional automaton is able to move its input head through its input word in four directions: upward, downward, leftward, and rightward. If we prevent the input head from moving upward, then we obtain a three-way two-dimensional automaton; preventing both upward and leftward movements results in a two-way two-dimensional automaton. While much is known about the decidability and complexity properties of the two-dimensional automaton model, the unary variant of this model is less studied. We show that the universality, equivalence, and inclusion problems for unary three-way deterministic two-dimensional automata are coNP-hard, while for the corresponding two-way model, the universality, equivalence, inclusion, and disjointness problems are in P. We further show that the universality, equivalence, and inclusion problems for unary two-way nondeterministic two-dimensional automata are coNP-hard and in ELEMENTARY; and the disjointness problem for the same model is NL-hard and in ELEMENTARY. Finally, we establish the decidability of a bounded variant of the universality problem for unary three-way nondeterministic two-dimensional automata, and show that this variant problem is coNP-complete.

2026-06-30T17:15:26Z Taylor J. Smith http://arxiv.org/abs/2607.00044v1 2026-06-29T19:14:23Z

We study a finite-state symbolic controller for systems in which the admissible visible transitions are fixed in advance and each visible state carries a minimum dwell requirement. The resulting model, which we call a destination-labeled self-looping system with dwell (DLSL system), records the visible graph together with local decision maps; dwell memory appears only after phase expansion. The main structural issue is that, once dwell is imposed, the current visible state no longer determines whether a departure is allowed. This leads to the converse problem: which deterministic transducers arise as phase-expanded realizations of DLSL systems over a fixed visible graph? We show that the answer is exactly the class of fiber-linear graph-respecting transducers. Under natural reachability and realizable-departure assumptions, equivalent accessible realizations over the same visible graph are isomorphic; in particular, the visible transduction determines the dwell vector and the local decision maps. We also prove that any graph-preserving deterministic realization enforcing dwell values $(d_i)$ requires exactly $\sum_i d_i$ control states. Finally, we give an $O(|Q||Ω|)$ recognition and reconstruction procedure, and extend the analysis to an edge-entry variant in which transitions may enter interior phases of successor fibers.

2026-06-29T19:14:23Z Reda Belaiche http://arxiv.org/abs/2606.30496v1 2026-06-29T16:02:02Z

A Pisot numeration system $U$ for $\mathbb N$ is a sequence of natural numbers generated by an integral homogeneous linear recurrence whose characteristic polynomial is the minimal polynomial of a Pisot number. The purpose of this paper is to introduce the analogue of the group of $p$-adic integers for such numerations when they \emph{preserve zeros}, which is equivalent to the `Condition F' introduced by Frougny and Solomyak for $β$-numerations. We show that these topological groups $\mathbb Z_U$ project homomorphically onto a torus. Equipping $\mathbb Z_U$ with the appropriate topology, we also show that if $U$ is unimodular, then $\mathbb Z_U$ is continuously isomorphic to a torus.

2026-06-29T16:02:02Z 29 pages, 4 figures Olivier Carton Jake Sudbery Reem Yassawi http://arxiv.org/abs/2503.21661v3 2026-06-29T15:58:19Z

Ontologies enable knowledge sharing and interdisciplinary collaboration by providing standardized, structured vocabularies for diverse communities. While logical axioms are a cornerstone of ontology design, natural language elements such as annotations are equally critical for conveying intended meaning and ensuring consistent term usage. This paper explores how meaning is represented in ontologies and how it can be effectively represented and communicated, addressing challenges such as indeterminacy of reference and meaning holism. To this end, instead of following the conventional approach of beginning with existing ontologies and working toward alignment or modularization, this article proposes a reversal of perspective: taking the ontological term as the starting point and introducing a new structure, named 'ontological unit', characterized by: a term-centered design; enhanced characterization of both formal and natural language statements; and an operationalizable definition of communicated meaning based on general assertions. By formalizing the meaning of ontological units, this work seeks to enhance the semantic robustness of terms, improving their clarity and accessibility across domains. Furthermore, it may offer a more effective foundation for ontology generation and significantly improves support for key maintenance tasks such as reuse and versioning. This article aims to establish the theoretical groundwork for the proposed approach and to lay the foundations for future applications in applied ontologies.

2025-03-27T16:24:12Z Paul Fabry Adrien Barton Jean-François Éthier 10.1177/15705838251391253 http://arxiv.org/abs/2606.30405v1 2026-06-29T14:51:03Z

A central goal of language theory is to compare formalisms by understanding their relative expressive power. One challenging question in this direction is the problem of determining the \emph{common fragment} of two formalisms $F_1$ and $F_2$, that is, effectively characterise the class $F_1\cap F_2$ of properties that can be expressed in both formalisms. A question closely related to this is the \emph{membership problem}, denoted $F_1 \membership F_2$, which asks whether a property expressed in $F_1$ can be also expressed in $F_2$. These problems become particularly difficult when \emph{branching-time} formalisms are involved. In this work, we prove that $\LTL \cap \PCTL$ is decidable, where \PCTL denotes \CTL extended with \emph{past operators}. We do this by showing that both membership problems, $\LTL \membership \PCTL$ and $\PCTL \membership \LTL$, are decidable. The direction $\PCTL \membership \LTL$ follows from suitable combinations of known results. The converse direction, $\LTL \membership \PCTL$, requires an automata-theoretic characterisation of $\PCTL$. Specifically, we introduce a new class of automata, called \emph{counter-free hesitant weak tree automata} ($\HWTcf$) that capture precisely the expressiveness of $\PCTL$, and that are obtained by combining two orthogonal restrictions on alternating parity tree automata, namely, \emph{counter-free hesitancy} and \emph{weakness}. We prove that, for every word language $L$ defined by an \LTL formula, the associated tree language $\triangle[L]$ is recognisable by an \HWTcf if and only if $L$ is recognized by a \DBW. Since the latter recognisability problem is decidable, so is the former. This result advances the longstanding open problem of deciding $\LTL \cap \CTL$. Indeed, that problem can now be reduced to $\PCTL \membership \CTL$, that is, the question of when past operators can be eliminated.

2026-06-29T14:51:03Z Extended version of the MFCS 2026 paper Massimo Benerecetti Dario Della Monica Angelo Matteo Fabio Mogavero Gabriele Puppis