SEARCH · arXiv Science

Results for “cs.FL”

Search indexed arXiv papers on artificial intelligence, large language models, computer vision and robotics. Read source abstracts and follow links to arXiv.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

7,800 records · Page 2Linked to original sources

arXiv2025

Store Languages of Turing Machines and Counter Machines

The store language of an automaton is the set of store configurations (state and store contents, but not the input) that can appear as an intermediate step in an accepting computation. A one-way nondeterministic finite-visit Turing machine (fvNTM) is a Turing machine with a one-way read-only input tape, and a single worktape, where there is some number $k$ such that in every accepting computation, each worktape cell is visited at most $k$ times. We show that the store language of every fvNTM is a regular language. Furthermore, we show that the store language of every fvNTM augmented by reversal-bounded counters can be accepted by a machine with only reversal-bounded counters and no worktape. Several applications are given to problems in the areas of verification and fault tolerance, and to the study of right quotients. We also continue the investigation of the store languages of one-way and two-way machine models where we present some conditions under which their store languages are recursive or non-recursive.

cs.FL↗

arXiv2026

Separating Words with Automata in the Half-adversarial Case

We consider the problem of separating words with deterministic finite automata (DFA) (Goral{č}{í}k and Koubek, 1986). This problem asks: given two distinct words $u,v$ of length at most $n$, what is the size of the smallest DFA that accepts one and rejects the other? The best upper bound on the worst-case over all pairs of words of length at most $n$ is $\tilde{O}(n^{1/3})$ states (Chase, 2021), while the best lower bound is $Ω(\log n)$. In this work, we consider the half-random, half-adversarial case: we show that if $u$ is a uniformly random binary word of length $n$, then with high probability, for any word $v$ not equal to $u$, there is a DFA with $O(\log^{7/3} n \mathrm{poly}\log\log n)$ states that separates $u$ and $v$. Our results are based on a novel analysis that exploits the structural sparsity of random words: we show how to apply block-wise compaction with small deterministic transducers to reduce the separation problem to the case of words with short run-length encodings.

cs.FL↗

arXiv2026

GreenFLag: A Green Agentic Approach for Energy-Efficient Federated Learning

Progressing toward a new generation of mobile networks, a clear focus on integrating distributed intelligence across the system is observed to drive performance, autonomy, and real-time adaptability. Federated learning (FL) stands out as a key emerging technique, enabling on-device model training while preserving data locality. However, its operation introduces substantial energy and resource demands. Energy needs are mostly met by grid power sources, while FL resource orchestration strategies remain limited. This work introduces GreenFLag, an agentic resource orchestration framework designed to minimize the energy consumption from the grid power to complete FL workflows, guarantee FL model performance, and reduce grid power reliance by incorporating renewable sources into the system. GreenFLag leverages a Soft-Actor Critic reinforcement learning approach to jointly optimize computational and communication resources, while accounting for communication contention and the dynamic availability of renewable energy. Evaluations using a real-world open dataset from Copernicus, demonstrate that GreenFLag significantly reduces grid energy consumption by 94.8% on average, compared to three state-of-the-art baselines, while primarily relying on green power.

cs.NI↗

arXiv2026

CEDAR: Automata as Verifiable Interfaces for Language-Guided Embodied Action

Natural-language tasking of embodied agents is rarely just goal specification: users also impose constraints that must persist while the world changes. Code-generating LLM agents can produce plausible behaviors for such instructions, but their free-form programs provide no stable object to verify, compose with new constraints, or repair from a failing trace. We present CEDAR, a counterexample-guided framework that grounds instructions as regular languages over environment event traces. CEDAR uses a language model for semantic judgments and execution traces for correction, then represents both skills and specifications as deterministic finite automata. This turns constraints into executable finite-state objects: a learned skill can be intersected with a learned sleep at night or stay in this biome specification, yielding a controller that enforces the learned constraint by construction rather than by repeated prompting. In Minecraft, with the same simulator/API observations available to a program-generating baseline, CEDAR maintains temporal and spatial constraints that the baseline fails to preserve and amortizes reuse of learned skills, reducing cumulative LLM queries. These results suggest that regular languages offer a practical verification layer between natural-language instructions and embodied-agent policies.

cs.AI↗

arXiv2026

NeuroSTAR: Automata-guided Neuro-symbolic Specification Formalization

Automated translation of natural language (NL) descriptions into Linear Temporal Logic over finite traces (LTLf) is a prerequisite for automated formal verification of a system's dynamic behavior. Several LLM-based methods have recently shown potential for this task. However, they struggle with the nuance of natural language descriptions, which can lead LLMs to only partially capture the intended meaning. To address this limitation, we propose NeuroSTAR (Automata-guided Neuro-symbolic Specification Formalization), an NL-to-LTLf framework that builds on two insights. First, it leverages multiple generators to obtain diverse LTLf candidates. Second, it uses an automata-theoretic semantic comparison based on DFA traces to identify behavioral disagreements that guide formula refinement. We evaluate NeuroSTAR and show that it improves NL-to-LTLf translation performance by 8-18 percentage points relative to the prior state-of-the-art (SoTA) on unambiguous benchmarks. We further study its applicability to a body of driving law text, a complex, realistic, and reference-free domain critical for autonomous-vehicle specification. This study shows that NeuroSTAR can capture the necessary temporal semantics in 83.9% of the driving law sections, which demonstrates the effectiveness of automata-guided reference-free refinement in formalization.

cs.FL↗

arXiv2026

Target Discounted Sum Problem on Markov Chains with Applications to Markov Decision Processes

The discounted sum is a way to aggregate a sequence of weights from a finite alphabet $Σ$, i.e., for a discount factor $λ$, the discounted sum of a sequence $w_0 w_1 w_2 \cdots$ over $Σ$ is $\sum_{i \in \mathbb{N}} w_i λ^i$. The target discounted-sum problem, which is currently open, asks, given $λ,Σ$ and a target $t$, whether there exists an infinite sequence over $Σ$ whose discounted sum is equal to $t$. We study and solve a probabilistic variant of this problem, i.e., the target discounted-sum problem on Markov chains. To do this, we prove that the event consisting of paths whose discounted sum is equal to the target and has infinitely many distinct suffix sums has probability zero. This structural property allows us to solve the target discounted-sum problem on Markov chains using an automata-theoretic technique. We apply our technical results to Markov decision processes with target discounted-sum objectives: we show that the infimum value and the finite-memory supremum value are computable in pseudo-polynomial time and are attained by deterministic finite-memory strategies.

cs.LO↗

arXiv2026

The Complexity of Coverability-Like Problems in Elementary Object Systems: Data-Nets to the Rescue

Elementary Object Systems (EOSs) are a model in the nets-within-nets (NWNs) paradigm, where tokens in turn can host standard Petri nets. We study the complexity of coverability-like problems, including termination and boundedness, over EOSs. Since coverability and boundedness are undecidable in general on EOSs, we focus on the relevant fragment of conservative EOSs (cEOSs). Our technique interprets cEOSs into the framework of data nets, whose tokens carry data from an infinite domain, thus bridging the nesting and the data-aware paradigms. Specifically, we show that cEOS coverability-like problems are equivalent to the coverability-like problems over an interesting fragment, called channel-$ν$PNs (c-$ν$PNs), of data nets that extends $ν$PN (featuring globally fresh name creation) with restricted forms of transfers with renaming. c-$ν$PNs remain less expressive than Unordered Data Nets, which feature lossy name creation as well as powerful forms of whole-place operations and broadcasts. These reductions allow us to analyze cEOS coverability taking advantage of known results on data nets. We conclude that the complexity of cEOS coverability is double-Ackermanian, $\mathcal{F}_{ω2}$-complete, while termination and boundedness are non-primitive recursive.

cs.CC↗

arXiv2026

Verification of $K$- and Infinite-Step Strong/Weak Anonymity Using Concurrent Compositions

Anonymity is an information flow property that provides privacy protection in the sense of non-uniqueness of system information at certain moments with respect to observations. The notion of $K$-step anonymity in the context of discrete-event systems characterizes the scenario that the state estimates cannot be a singleton within at most $K$ observational steps prior to the current instant, while infinite-step anonymity is the same as $K$-step anonymity without considering the limit on $K$. In this paper, we lucubrate $K$- and infinite-step anonymity for partially-observed discrete-event systems modeled by non-deterministic finite-state automata. First, we define two strong types and two weak types of $K$- and infinite-step anonymity that are fundamentally different from the existing notions of $K$- and infinite-step anonymity due to the consideration of strong and weak anonymous projections. Then, we develop a new methodology by exploiting the concurrent-composition technique to verify these four types of anonymity. Based on the constructed concurrent compositions, verifiable necessary and sufficient conditions for the four types of anonymity are provided, along with their complexity analysis. Finally, the upper bounds on $K$ for $K$-step strong anonymity and weak anonymity are computed.

cs.FL↗

arXiv2026

Representing One Letter Weighted Automata Over the Tropical Semiring

We consider weighted automata over the tropical semiring $\mathbb{Z}_\infty(min, +)$. Recently, it was shown that determinisation is decidable; in this paper we focus on the complexity when the alphabet is unary. In 2001, Lombardy showed this problem is decidable, a close inspection of his proof yields a coNP upper bound on the complexity. Earlier Gaubert showed that every weighted automaton in this setting can be effectively turned into an equivalent union of deterministic weighted automata. We prove Gaubert's result efficiently, presenting it as a generalisation of Chrobak's normal form for unary NFA. In particular, we prove that the equivalent union of deterministic weighted automata can be represented by a weighted automaton of quadratic size in the size of the original one, and this representation can be computed in polynomial time. Building on this, we show that determinisation, and even register minimisation (which generalises determinisation), is coNP-complete. We complete the paper with observations that the boundedness problem is also coNP-complete by reductions with determinisation. Lastly, we provide evidence that all of these problems are not FPT (by proving $coW_1$-hardness) when parametrised by the number of deterministic automata in the union.

cs.FL↗

arXiv2026

Exact Accepting-State Spectrum for Reversal of Permutation Automata

We determine the accepting-state spectrum of reversal for permutation automata exactly, thereby proving the Rauch--Holzer conjecture on this operation. For every $m \ge 2$ and every $α\ge 2$, we construct a binary permutation automaton $A_{m,α}$ such that $\operatorname{asc}(L(A_{m,α}))=m$ and $\operatorname{asc}(L(A_{m,α})^R)=α$. Combined with the trivial cases $m=0$ and $m=1$, and with the previously known fact that $1$ is magic for every $m \ge 2$, this yields the exact spectrum $g^{\operatorname{asc}}_{R,\mathrm{PFA}}(0)=\{0\}$, $g^{\operatorname{asc}}_{R,\mathrm{PFA}}(1)=\{1\}$, and $g^{\operatorname{asc}}_{R,\mathrm{PFA}}(m)=\mathbb{N}_{\ge 2}$ for every $m \ge 2$. Thus reversal has, for permutation automata, the simplest possible exact accepting-state spectrum compatible with the single nontrivial obstruction at value $1$. The proof uses a uniform group-theoretic witness family: the states of the forward automaton are the $α$-subsets of $[n]$, where $n=m+α-1$, under the action generated by an $n$-cycle and a transposition, while the accepting states form a single star family. After reversal, the reachable subset-states are exactly the stars. This makes it possible to count the accepting reachable states precisely and to prove minimality of the reachable reverse automaton.

cs.FL↗

arXiv2026

Adaptive Strategies for GR(1) Games

We consider two-player GR(1) games on graphs, where the system player Eve must satisfy \[ \Box\Diamond A_1\land\cdots\land\Box\Diamond A_m \;\implies\; \Box\Diamond G_1\land\cdots\land\Box\Diamond G_n \] against the environment player Adam. Here $A_1,\ldots,A_m$ are assumptions on the environment, $G_1,\ldots,G_n$ are guarantees the system must provide, and $\Box\Diamond S$ denotes ``always eventually $S$''. Traditional static strategies are overly conservative: they may actively violate assumptions to trivially satisfy the implication, or abandon all guarantees when any assumption is violated. Existing methods to prevent such behaviors incur doubly exponential blowup. We introduce an adaptive framework treating Adam as a non-adversarial agent with unknown objectives. Eve monitors which assumptions Adam actually meets and adapts her strategy at runtime to maximize satisfied guarantees. Central to our approach is a novel algorithm for monitoring liveness properties $\Box\Diamond S$, enabling Eve to maintain real-time likelihood estimates of which assumptions will be fulfilled. Eve pre-computes strategies optimal for different assumption subsets, deploying a probability distribution over them that dynamically adjusts based on monitor outputs. We prove that when assumptions are violated, Eve's randomized adaptive strategy converges asymptotically to the deterministic strategy maximizing guarantees. A prototype demonstrates effectiveness and superior computational performance compared to the state of the art.

cs.LO↗

arXiv2026

Relative Prime Factorization and Finite-State Presentations under Fixed Finite-Monoid Observation

Let $L\subseteqΣ^*$ and fix a morphism $h:Σ^*\to M$ into a finite monoid. We study exact factorization and canonical presentation in the relative syntactic congruence $θ_{L,h}:=\equiv_L\cap\ker h$. We separate unique factorization from finite direct presentation. An exhaustively computer-checked $36$-element quotient has a unique exact prime factorization for every live non-unit class, yet its valid prime-return rules contain an infinite family, so unique factorization does not imply the finite relative presentation property (FRP), even for a finite quotient. We lift the same defect to a nonregular context-free language with an infinite relative quotient and finite prime spectrum. To isolate the obstruction, we introduce the finite-state relative presentation property (FSRP), in which canonical valid right-hand-side languages are represented by finite residual controllers, and prove $\mathrm{FRP}\subsetneq\mathrm{FSRP}$. We then introduce prime-target left-division determinism (PTLD), which implies unique exact factorization, tail exactness, tail determinism, and a quadratic bound on valid rules. A nonregular deterministic context-free example with a finite group observer satisfies PTLD while lying outside every fixed $(k,\ell)$-substitutable class. Finally, for fixed $h$ we give a strong positive-data learner for the canonical PTLD presentation with polynomial-time hypothesis updates and a finite characteristic sample, together with a limit reconstruction of the canonical FSRP controller from weakly behaviorally correct CFG-valued learners.

cs.FL↗

arXiv2026

Separating Parsing Expression Grammars using Cell-Probe Lower Bounds

We resolve three open problems concerning parsing expression grammars (PEGs). We construct a single language $C$ satisfying $C\in\mathsf{LIN}\cap\mathsf{PEG}$ and $C^R\in\mathsf{LIN}\setminus\mathsf{PEG}$. This proves that some linear context-free language is not a PEG language and that PEG languages are not closed under reversal, confirming a conjecture of Loff, Moreira, and Reis. Factoring the same witness resolves the concatenation-closure problem of Rubtsov and Chudinov negatively, in the strong form $\mathsf{PEG}\cdot\mathsf{REG}\not\subseteq\mathsf{PEG}$ despite $\mathsf{REG}\cdot\mathsf{PEG}\subseteq\mathsf{PEG}$. It also refutes closure under Kleene star, homomorphisms, and substitutions. Our main technique converts scaffolding automata (SCAs), which characterize reversals of PEG languages, into dynamic data structures in the cell-probe model. For any suitably local serialization of a problem with preprocessing, updates, and a final Boolean query, an SCA recognizer yields an exact deterministic cell-probe data structure whose operation costs are proportional to the corresponding encoding lengths. Cell-probe lower bounds can therefore prove SCA non-membership and, by reversal, PEG non-membership. We apply this transfer to Multiphase Inner Product using one-symbol update blocks and a query suffix of length $O(\log n)$, while keeping both the language and its reversal linear context-free. Ko's cell-probe lower bound then yields the witness above. The arguments are additionally formalized in Lean 4.

cs.PL↗

arXiv2026

On Good-for-MDPs Automata

Nondeterministic good-for-MDPs (GFM) automata are for MDP model checking and reinforcement learning what good-for-games (GFG) automata are for reactive synthesis: a more compact alternative to deterministic automata that displays nondeterminism, but only so much that it can be resolved locally, such that a syntactic product can be analysed. GFM has recently been introduced as a property for reinforcement learning, where the simpler Büchi acceptance conditions it allows to use is key. However, while there are classic and novel techniques to obtain automata that are GFM, there has not been a decision procedure for checking whether or not an automaton is GFM. We show that GFM-ness is decidable and provide an EXPTIME decision procedure as well as a PSPACE-hardness proof. We also compare the succinctness of GFM automata with other types of automata with restricted nondeterminism. The first natural comparison point are GFG automata. Deterministic automata are GFG, and GFG automata are GFM, but not vice versa. This raises the question of how these classes relate in terms of succinctness. GFG automata are known to be exponentially more succinct than deterministic automata, but the gap between GFM and GFG automata as well as the gap between ordinary nondeterministic automata and those that are GFM have been open. We establish that these gaps are exponential, and sharpen this result by showing that the latter gap remains exponential when restricting the nondeterministic automata to separating safety or unambiguous reachability automata.

cs.FL↗

arXiv2026

Behavioral Memory under Symmetry in One-Way Quantum Automata

Under compact symmetry, observable behavior reduces to an invariant operator algebra, but its dimension is not yet classical memory: some coordinates are dynamically frozen, some invisible to threshold tests, and some already classical. We develop an operator-algebraic theory that separates these effects through three filters. For one automaton, behavior is the Hilbert--Schmidt pairing between prefix-reachable states and suffix-observable effects, whose rank equals the real Hankel rank without controllability or observability assumptions. Maximizing this invariant over a symmetry-constrained dynamical class gives a structural capacity controlled by the symmetry commutant: its center stores isotypic populations frozen by reversible dynamics, its traceless multiplicity blocks carry movable noncommutative coordinates, dissipation removes the unary spectral loss inside those blocks, and covariant mobility releases relative populations subject to component conservation. Operational realization then determines which surviving coordinates force probabilistic states. For a fixed nontrivial invariant readout, full mobility gives an exact dichotomy in worst-case state cost: a commutative invariant algebra costs exactly its dimension, whereas a noncommutative multiplicity block raises the unrestricted cost by exactly one state. Thus noncommutativity has a one-state worst-case classical price. The known four-letter quadratic-plus-one law at trivial symmetry is the fully mobile endpoint of this principle. Schur--Weyl duality further shows that different preserved symmetries on the same tensor-power Hilbert space can change the worst memory scale from polynomial to exponential, while fixed-weight modules give an exact Catalan law at half filling, with structural capacity equal to the Catalan count minus its central-sector correction.

cs.FL↗

arXiv2026

Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations

We study a family of language operations based on insertion, shuffle, and crossover and investigate the undecidability of adjacent equality together with finite convergence and associated spectrum questions. Insertion and shuffle operations on formal languages arise in formal language theory, models of concurrency, and biologically inspired computation. This paper studies a different question from the usual closure problem, specifically whether an increasing sequence of languages generated by repeated insertion, or by increasing the permitted degree of bounded shuffle, reaches an instance of adjacent equality after finitely many stages. We show that several such adjacent equality questions are undecidable. In particular, reaching such an adjacent equality event is undecidable for each of the following: iterated insertion of a regular language into a context-free language; bounded shuffle of a regular language with a context-free language as the bound increases; and the corresponding self-insertion and self-bounded-shuffle hierarchies for context-free languages. The new reductions proceed directly from the undecidability of context-free-language universality, using separator-delimited block constructions and, for self-operations, an absorbing regular language of guard violations. Earlier trace-based proofs relied on mortality and uniform halting. More generally, we investigate finite-stage equality and stabilization (persistent equality) in hierarchies generated by insertion and bounded shuffle. In addition to giving substantially simpler proofs of earlier undecidability results, we obtain general criteria for one-step equality, develop new reductions for self-insertion, and identify several open problems, including structural questions concerning insertion depth and degree whose resolution determines whether adjacent equality necessarily implies permanent stabilization.

cs.FL↗

arXiv2026

Finite-Monoid Compression in Syntactic Concept Lattices: Arity Hierarchies and a Pseudovariety Trichotomy

Clark's syntactic concept lattice (SCL) records two-sided distributional structure, and Wurm extended it to tuples of arbitrary finite arity. We study $\operatorname{cmp}_f(L)$, the minimum image size of a finite-monoid observation that preserves guarded tuple substitution through arity $f$ on the principal layer. For regular languages, we characterize $\operatorname{cmp}_f(L)$ exactly as the least cardinality of the codomain of an $f$-separating relational morphism from the pointed syntactic monoid. Let $\operatorname{ch}(\mathbf V)$ denote the least arity at which these compression numbers stabilize uniformly over a pseudovariety $\mathbf V$. Our main result is the following trichotomy of possible uniform heights: $\operatorname{ch}(\mathbf V)\in\{1,2,\infty\}$, with $\operatorname{ch}(\mathbf V)=\infty$ if and only if $\operatorname{Synt}(\{ab\})\in\mathbf V$. Thus no finite uniform compression height $3,4,\ldots$ occurs. The infinite case is sharp: inside $\langle\operatorname{Synt}(\{ab\})\rangle$, every boundary $d\to d+1$ admits unbounded compression gaps, and arbitrary finite strict prefixes of the arity hierarchy are realizable. On the finite side, commutative monoids and bands stabilize at arity one, while every completely regular syntactic monoid stabilizes by arity two; finite group kernels show that the binary bound is sharp. At unary arity, every nonempty finite simple graph is realized by an explicit length-three language, yielding an exact chromatic-number formula and NP-completeness of deciding $\operatorname{cmp}_1(L)\le 3$ for explicitly listed length-three languages. The structural boundary between compression heights one and two remains open.

cs.FL↗

arXiv2026

Spectral and combinatorial methods for efficiently computing the rank of unambiguous finite automata

A zero-one matrix is a matrix with entries from $\{0, 1\}$. We study monoids containing only such matrices. A finite set of zero-one matrices generating such a monoid can be seen as the matrix representation of an unambiguous finite automaton, an important generalisation of deterministic finite automata which shares many of their good properties. Let $\mathcal{A}$ be a finite set of $n \times n$ zero-one matrices generating a monoid of zero-one matrices, and $m$ be the cardinality of $\mathcal{A}$. We study the computational complexity of computing the minimum rank of a matrix in the monoid generated by $\mathcal{A}$. By using linear-algebraic techniques, we show that this problem is in $\textsf{NC}$ and can be solved in $\mathcal{O}(mn^4)$ time and $\mathcal{O}(n^2)$ space. We also provide a combinatorial algorithm finding a matrix of minimum rank in $\mathcal{O}(mn^4)$ time and $\mathcal{O}(n^3)$ space. As a byproduct, we show a very weak version of a generalisation of the Černý conjecture: there always exists a straight line program of size $\mathcal{O}(n^2)$ describing a product resulting in a matrix of minimum rank. For the special case corresponding to total DFAs (that is, for the case where all matrices have exactly one 1 in each row), the minimum rank is the size of the smallest image of the set of all states under the action of a word. Our combinatorial algorithm finds a matrix of minimum rank in time $\mathcal{O}(n^3 + mn^2)$ in this case.

cs.FL↗