https://arxiv.org/api/vUTCgJoWqXaA9UuWZG0xcLr0TqY 2026-07-21T08:25:29Z 6101 60 15 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 http://arxiv.org/abs/2602.07964v2 2026-06-29T12:28:39Z

Over the years, bisimulations have emerged as a pervasive paradigm, finding applications in numerous areas, including concurrency theory, model checking, automata theory, logic, programming languages and category theory. In this paper, we establish a connection between bisimulations and data compression. More precisely, we study the relationship between bisimulations and Wheeler automata (Alanko et al., SODA 2020), a class of automata that has received considerable attention in recent years. The standard notion of bisimulation is not appropriate, so we introduce Wheeler bisimulations, that is, bisimulations that respect the convex structure of the considered Wheeler automata. We show that Wheeler bisimilarity induces a unique minimal Wheeler NFA (analogously to standard bisimulations). In particular, in the deterministic case, we retrieve the minimal Wheeler deterministic automaton of a given language. We also show that the minimal Wheeler NFA induced by Wheeler bisimulations can be built in linear time. This is in contrast with standard bisimulations, for which the corresponding minimal NFA can be built in $ O(m \log n) $ time (where $ m $ is the number of edges and $ n $ is the number of states) by adapting Paige-Tarjan partition refinement algorithm. Compared to previous state-reduction techniques, our bisimulation-induced construction is the first for which (i) we obtain a canonical Wheeler NFA and (ii) the resulting Wheeler NFA can be built in linear time.

2026-02-08T13:23:15Z Nicola Cotumaccio http://arxiv.org/abs/2606.30042v1 2026-06-29T09:35:53Z

Vector Addition System with States (VASS) are a ubiquitous model of infinite-state systems consisting of a set of non-negative counters which can be incremented and decremented. It is known that the reachability problem for VASS is Ackermann-complete. Because of this huge complexity, various over-approximations of VASS have been studied in the literature. One such over-approximation is continuous VASS (CVASS), in which the counters are (non-negative) rational numbers and whenever a vector is added to the current counter values, it is first scaled with an arbitrarily chosen rational factor between zero and one. It is known that the reachability problem for CVASS is $\mathsf{NP}$-complete. In this paper, we initiate the study of fixed-dimensional CVASS, i.e., CVASS with a fixed number of counters. We study both the reachability and coverability problems, under both unary and binary encodings as well as over both the non-negative and the rational semantics. This gives rise to a collection of eight different problems. As our main result, we prove a complexity dichotomy for all of these eight problems when the transition vectors are over the rationals: For dimension 1, all of the eight problems are in $\mathsf{AC}^1$, whereas for any dimension at least 2, all of the eight problems are $\mathsf{NP}$-complete. Furthermore, the hardness holds even when the underlying automaton is acyclic. To achieve this result, we present a new technique called the Egyptian prime fractions technique. Finally, we also study these problems when the transition vectors are over the integers. Except for dimension 2, we classify the complexity of these problems over the non-negative semantics: For dimension 1, all of the problems are in $\mathsf{AC}^1$, whereas for dimensions 3 and above, all of the problems are $\mathsf{NP}$-complete.

2026-06-29T09:35:53Z Abstract shortened to fit arXiv requirements Michal Ajdarów A. R. Balasubramanian Łukasz Orlikowski http://arxiv.org/abs/2606.30013v1 2026-06-29T09:19:06Z

Suppose we have a deterministic finite-state transducer $A$ and an infinite word $x$, and run $A$ on $x$ to obtain an infinite word $A(x)$. Which properties of $x$ are guaranteed to also hold for $A(x)$? In this paper, we study this preservation question for various well-known combinatorial properties, e.g., recurrence, being morphic, and having factor frequencies. The celebrated Krohn-Rhodes theorem provides the framework for proving our preservation results, and our techniques are based on the ergodic theory of symbolic dynamical systems, i.e., shift spaces.

2026-06-29T09:19:06Z Valérie Berthé Herman Goulet-Ouellet Toghrul Karimov Dominique Perrin Mihir Vahanwala http://arxiv.org/abs/2604.24151v2 2026-06-29T09:13:43Z

Series-parallel (SP) graphs are binary edge-labeled graphs with a designated source and target vertex, built using serial and parallel composition. A set of graphs is recognizable if membership depends only on its image under a homomorphism into a finite algebra. For SP-graphs, and more generally, for graphs of bounded tree-width, recognizability coincides with definability in Counting Monadic Second-Order (CMSO) logic. Despite this strong logical characterization, the conciseness and algorithmic effectiveness of syntactic representations of recognizable sets of SP (and bounded-tree-width) graphs remain poorly understood. Building on previously introduced regular grammars for SP-graphs, we show that recognizable sets admit concise and effective syntactic representations. The main contribution is an improved construction of finite recognizer algebras whose size is singly-exponential in the size of a regular grammar, improving upon the previously known double-exponential bound. As a consequence, the problems of intersection and language inclusion for sets represented by regular grammars are shown to be EXPTIME-complete, thus improving on a previously known 2EXPTIME upper bound.

2026-04-27T08:07:38Z Marius Bozga Radu Iosif Florian Zuleger http://arxiv.org/abs/2605.15390v2 2026-06-29T08:21:05Z

We present Kofola, an efficient tool for complementation and inclusion checking of Büchi automata, two central tasks in automata-theoretic verification with applications in model checking, monitoring, and theorem proving. Kofola implements a state-of-the-art modular complementation framework that decomposes the input automaton into strongly connected components and applies to each component a complementation algorithm tailored to its structural properties. Building on this modular construction, Kofola also provides modular inclusion checking with new heuristics. A key ingredient is a new on-the-fly emptiness-checking algorithm for the simple generalized Rabin pair condition produced by our complementation, allowing the search to terminate as soon as the explored state space suffices. Empirical evaluation shows that Kofola is highly competitive with state-of-the-art complementation and inclusion-checking tools: it is the most robust tool in our evaluation and often outperforms competitors by several orders of magnitude on benchmarks from practical applications.

2026-05-14T20:19:30Z accepted at CAV'26 Ondrej Alexaj Vojtěch Havlena Lukáš Holík Ondřej Lengál Yong Li Nicolas Mazzocchi http://arxiv.org/abs/2605.25253v2 2026-06-29T08:17:01Z

Higher-dimensional automata (HDA) are a model of concurrency that models simultaneous execution of events using higher dimensional cells. HDA recognize languages of pomsets, a generalization of finite words whose letters are partially ordered. We prove a new algebraic characterization of HDA languages: a language of pomsets is regular if and only if it is the inverse image of a functor from the category of pomsets into a finite category. Furthermore, the language is definable in first-order logic exactly when it is recognized by an aperiodic category, generalizing the McNaughton-Papert theorem to HDA languages. We also investigate a notion of counter-free HDA, and show that if a language is accepted by a counter-free HDA, it must be definable in first-order logic. The converse, however, is still open.

2026-05-24T20:47:02Z Enzo Erlich Jérémy Ledent Krzysztof Ziemiański http://arxiv.org/abs/2606.29939v1 2026-06-29T08:15:50Z

In this work, we generalize Kleene's theorem from free single-sorted algebras to free many-sorted algebras. Our main result establishes that, under appropriate finitary assumptions, a language of a given sort in a free many-sorted algebra is recognizable if and only if it is regular.

2026-06-29T08:15:50Z 35 pages Lü Gong Raúl Ruiz Mora Nofre Sanmartín Vich Enric Cosme Llópez