https://arxiv.org/api/Q6PEIHxqUkLy+6uWfau6NRsAXtQ 2026-07-20T04:33:58Z 6096 30 15 http://arxiv.org/abs/2607.08795v1 2026-07-08T12:34:31Z

Redundancy in non-standard numeration systems is often associated with robustness, but its practical value in finite digital arithmetic depends on how representation, storage, and repair are defined. We study intrinsic redundancy in finite beta-expansion systems using a bounded-window model that separates semantic non-uniqueness from canonical codebook admissibility. The model distinguishes arithmetic canonicalization from corruption repair and evaluates structural detectability, value-preserving repair of the observed state, and survival of the original value. For the golden-ratio system and related multinacci bases, we prove that a genuine single-digit corruption in a canonically injective finite codebook cannot be semantically recovered by exact repair without external information. Semantic survival under exact structural repair is possible only for localized multi-digit perturbations corresponding to algebraic rewrite identities, such as the equivalence of 100 and 011. Experiments comparing standard binary, signed-digit non-adjacent form, and multinacci systems quantify trade-offs among codebook sparsity, fault visibility, canonicalization cost, residual error, and boundary loss. The results show that intrinsic beta-redundancy is a constrained-language resource for structural digital integrity rather than a substitute for classical error-control redundancy.

2026-07-08T12:34:31Z 73 pages, 12 figures. Code and experiment scripts are available at https://doi.org/10.5281/zenodo.21140212 Adilbek Taizhanov Miras Seilkhan http://arxiv.org/abs/2604.10124v7 2026-07-08T11:59:48Z

In [7], a constraint on invariant measures of bi-permutative cellular automata has been observed: fixed values at the positive indices determine almost-surely a uniform conditional probability on the subset of values of positive conditional probability at the zero index. When the alphabet is a finite group and the automaton is multiplication of two neighbors, that set is in fact a coset of some subgroup. In the present paper, we strengthen the formulations in [7] and investigate further the implications of this constraint. In the finite group case mentioned above, relations between some attributes of the group structure and the invariant measures are examined. We also inspect a factor, with respect to the shift, that this constraint induces, and analyze the special case in which it has zero measure-theoretical entropy, thus observing an interplay between existence of zero entropy invariant measures on that factor and existence of positive entropy measures corresponding to them on the original system. Then, we leave the setting of bi-permutative cellular automata and generalize our results to a wider class which we named RLP subshifts. The peculiar situation is that although this class may be much larger than the class of bi-permutative cellular automata, we were able to prove only for essentially one other example - the symbolic coding of the times 2 times 3 system on the circle (and its generalizations) - that it belongs to it.

2026-04-11T09:38:43Z Matan Tal http://arxiv.org/abs/2607.05701v2 2026-07-08T03:30:15Z

We study sets and functions definable in the three additive theories $\FO(\Z,+,\leq)$, $\FO(\R,+,\leq)$, and $\FO(\R,\Z,+,\leq)$. The Ginsburg--Spanier theorem~\cite{GS66} characterizes $\FO(\Z,+,\leq)$-definable sets as exactly the semi-linear sets. We extend this characterization in two directions. First, we show that $\FO(\Z,+,\leq)$-definable \emph{functions} are exactly the piecewise linear functions (Theorem~\ref{thm:integer}), and that $\FO(\R,+,\leq)$-definable functions are also exactly the piecewise linear functions (Theorem~\ref{thm:real}). The proofs are direct algebraic arguments using only a stability lemma and the Ginsburg--Spanier theorem. Second, we introduce \emph{semi-polinear sets} as the $\FO(\R,\Z,+,\leq)$ analogue of semi-linear sets, and prove that the class of mixed-linear sets and the class of semi-polinear sets coincide (Theorem~\ref{thm:mixed-sets}). We further show that $\FO(\R,\Z,+,\leq)$-definable functions are exactly the \emph{piecewise-simple} functions (Theorem~\ref{thm:mixed-functions}), a new class of functions that are linear in the integer part and in the fractional part of the argument, but with potentially different linear coefficients for each. These algebraic characterizations unify the three theories in a single framework, and the proofs are purely algebraic, without reference to automata or machines.

2026-07-06T23:47:19Z 12 pages, 1 table LMCS format Alain Finkel Jérôme Leroux http://arxiv.org/abs/2307.06777v4 2026-07-07T17:37:09Z

The study of rational relations is fundamental to the study of formal languages and automata theory. A rational relation is conjugate if each pair of words in the relation is conjugate (or cyclic shifts of each other). The notion of conjugacy has been central in addressing many important algorithmic questions about rational relations. We address the problem of checking whether a rational relation is conjugate and show that it is decidable. Towards our decision procedure, we establish a new result that is of independent interest to word combinatorics. We identify a necessary and sufficient condition for the set of pairs given by $(a_0,b_0) G_1^* (a_1,b_1) \cdots G_k^*(a_k,b_k), k \geq 0$ to be conjugate, where $G_i$ is a (not necessarily rational) conjugate relation and $a_i, b_i$ are arbitrary words. This is similar to, and a nontrivial generalisation of, a characterisation given by Lyndon and Schützenberger in 1962 for the conjugacy of a pair of words. Furthermore, our condition can be evaluated in polynomial time, yielding a PTIME procedure for deciding the conjugacy of a rational relation given as a sumfree expression. Since any arbitrary rational expression can be expressed as a sum of sumfree expressions (with an exponential blow-up), decidability of conjugacy of rational relations follows.

2023-07-13T14:34:18Z C. Aiswarya Amaldev Manuel Saina Sunny http://arxiv.org/abs/2607.06341v1 2026-07-07T14:39:59Z

Formal verification offers the strongest guarantee of software correctness, but it does not scale: the proofs demanded by interactive theorem provers such as Coq require enormous expert effort. Large language models (LLMs) promise to generate these proofs automatically, yet existing approaches wire a fixed, human-designed proof strategy into the system and constrain the model to follow it (retrieving premises and predicting tactics one step at a time, or splitting goals by divide-and-conquer), and still prove only a fraction of their target theorems. We show that imposing such a strategy is unnecessary and limiting. Handing the whole lemma to a general LLM code agent (for example, Claude Code), free to choose its own approach, and wrapping it in a verification harness is both simpler and more effective, achieving full coverage: every targeted lemma proved, with no failures and no Coq expert intervention. The agent writes the proofs under feedback and hard constraints from the harness that keep each one sound (accepted only when the prover's kernel closes it), complete (no obligation left unproved or silently dropped), and terminating (no divergent tactics). We evaluate this harness plus code agent along three dimensions. (1) Core logic: on Iris, the state-of-the-art separation logic for concurrent and memory-manipulating programs, Aria proves all 4,257 lemmas of the four core modules and the 217 lemmas verifying Rust's standard libraries built on it, fully automatically. (2) Comparison with prior LLM provers: on reglang, where prior provers manage barely one in eight, Aria proves all 318. (3) Generality: on iris-lean, the unfinished Lean 4 port of Iris, it proves 72 not-yet-ported lemmas, showing the approach is not specific to Coq. A state-of-the-art model (Claude Opus 4.7) can write proofs for verified software development fully and automatically.

2026-07-07T14:39:59Z Shuangxiang Kan Shuanglong Kan Sebastian Ertel http://arxiv.org/abs/2511.09703v2 2026-07-07T12:33:57Z

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.

2025-11-12T20:00:48Z Stefan Kiefer Andrew Ryzhikov http://arxiv.org/abs/2607.06155v1 2026-07-07T11:32:56Z

Modern sequence models are increasingly deployed as agents that interleave token generation with calls to external tools. We give an exact, architecture-level account of when such tool access increases computational expressivity. We model any fixed finite-precision recurrent sequence model, including finite-precision state-space models (SSMs) with $B$ bits of internal state, as a deterministic finite-state controller interacting with an oracle through a finite command/observation interface. Our results form a sharp dichotomy. First, tools that are themselves finite-state add essentially nothing: a product-state simulation internalizes any finite-state bounded-interface oracle with finite memory set $M$ at a cost of only $\log_2 |M| + O(1)$ additional bits, so the augmented system remains finite-state. Second, a single minimal infinite-state tool, namely a tape supporting only local $\mathtt{read}$, $\mathtt{write}$, and $\mathtt{move}$ commands, makes the system Turing complete: for every single-tape Turing machine with state set $Q$ and tape alphabet $Γ$, a controller with $O(\log |Q| + \log |Γ|)$ bits of internal memory simulates it, and we exhibit a concrete exponential separation: $\mathrm{EQ}_n$ requires $2^n$ states without tools but a single constant-size controller with the tape tool. Third, we show that this construction is realized exactly by a natural one-layer finite-precision selective affine SSM controller with binary one-hot hidden states, $\{0,1\}$ transition matrices, and zero biases. Selectivity is essential to the construction. In the supplementary material, we make all constants explicit, prove a logarithmic oracle-assisted universal simulation, where $O(\log B)$ recurrent bits suffice to simulate any $B$-state Turing machine, and prove a matching impossibility result.

2026-07-07T11:32:56Z 24 pages Nikola Zubić Qian Li Yuyi Wang Davide Scaramuzza http://arxiv.org/abs/2503.05006v2 2026-07-07T09:22:55Z

Markov decision process over vector addition system with states (VASS MDP) is a finite state model combining non-deterministic and probabilistic behavior, augmented with non-negative integer counters that can be incremented or decremented during each state transition. VASS MDPs can be used as abstractions of probabilistic programs with many decidable properties. In this paper, we develop techniques for analyzing the asymptotic behavior of VASS MDPs. That is, for every initial configuration of size \(n\), we consider the number of transitions needed to reach a configuration with some counter negative. We show that given a strongly connected VASS MDP there either exists an integer \(k\leq 2^d\cdot 3^{|T|} \), where \(d \) is the dimension and \(|T|\) the number of transitions of the VASS MDP, such that for all \(ε>0 \) and all sufficiently large \(n\) it holds that the complexity of the VASS MDP lies between \(n^{k-ε} \) and \(n^{k+ε} \) with probability at least \(1-ε\), or it holds for all \(ε>0 \) and all sufficiently large \(n\) that the complexity of the VASS MDP is at least \(2^{n^{1-ε}} \) with probability at least \(1-ε\). We show that it is decidable which case holds and the \(k\) is computable in time polynomial in the size of the considered VASS MDP. We also provide a full classification of asymptotic complexity for VASS Markov chains.

2025-03-06T22:15:13Z Michal Ajdarów http://arxiv.org/abs/2508.20735v2 2026-07-07T08:48:09Z

We study parallel algorithms for the minimisation and equivalence checking of Deterministic Finite Automata (DFAs). Regarding DFA minimisation, we implement four different massively parallel algorithms on Graphics Processing Units~(GPUs). Our results confirm the expectations that the algorithm with the theoretically best time complexity is not practically suitable to run on GPUs due to the large amount of resources needed. We empirically verify that parallel partition refinement algorithms from the literature perform better in practice, even though their time complexity is worse. Furthermore, we introduce a novel algorithm based on partition refinement with an extra parallel partial transitive closure step and show that on specific benchmarks it has better run-time complexity and performs better in practice. In addition, we address checking the language equivalence and inclusion of two DFAs. We consider the Hopcroft-Karp algorithm, and explain how a variant of it can be parallelised for GPUs. We note that these problems can be encoded for the GPU-accelerated model checker \GPUexplore, allowing the use its lockless hash table and fine-grained parallel work distribution mechanism.

2025-08-28T12:58:17Z 28 pages, 10 figures, 5 tables Jan Heemstra Jan Martens Anton Wijs http://arxiv.org/abs/2607.05907v1 2026-07-07T07:02:13Z

Spot is a mature, open-source C++/Python library and toolset for Linear Temporal Logic (LTL) and $ω$-automata manipulation. While Spot is routinely used as a research and verification back-end, its rich visualization capabilities and Python interface also make it an attractive platform for \emph{teaching} the connections between temporal logic formulas and the $ω$-automata that give them their semantics.

2026-07-07T07:02:13Z Demonstration for TEAL'26 Alexandre Duret-Lutz http://arxiv.org/abs/2502.12307v2 2026-07-06T19:58:48Z

For a fixed alphabet $A$, an infinite sequence $X$ is said to be normal if every word $w$ over $A$ appears in $X$ with the same frequency as any other word of the same length. A classical result of Agafonov (1966) relates normality to finite automata as follows: a sequence $X$ is normal if and only if any subsequence of $X$ selected by a finite automaton is itself normal. Another theorem of Schnorr and Stimm (1972) gives an alternative characterization: a sequence $X$ is normal if and only if no gambler can win large amounts of money by betting on the sequence $X$ using a strategy that can be described by a finite automaton. Both of these theorems are established in the setting of deterministic finite automata. This raises the question as to whether they can be extended to the setting of probabilistic finite automata. In the case of the Agafonov theorem, this question was positively answered by Léchine et al. (2024) in a restricted case of probabilistic automata with rational transition probabilities. In this paper, we settle the full conjecture by proving that both the Agafonov and the Schnorr-Stimm theorems hold true for arbitrary probabilistic automata. Specifically, we show that a sequence $X$ is normal if and only if any probabilistic automaton selects a normal subsequence of $X$ with probability $1$. We also show that a sequence $X$ is normal if and only if a probabilistic finite-state gambler fails to win on $X$ with probability $1$.

2025-02-17T20:26:55Z Laurent Bienvenu Hugo Gimbert Subin Pulari http://arxiv.org/abs/2607.05076v1 2026-07-06T13:39:00Z

Formal verification is seldom applied to production software, because writing and maintaining a model has historically cost more than it returns. A companion study [1] extended SysMoBench [4] with a lower-cost alternative: specifications are graded against traces captured from the running system. It found that when large language models write the specifications, reliability is governed by the structure of the specification contract, not the language. This paper evaluates both on production software: the payment workflow of an operational restaurant point-of-sale system, which must keep the register, payment terminal, and payment processor in agreement. We report three results. First, the core protocol is correct relative to a hand-built, line-cited model under a precisely stated failure model. The audit found seven failure-handling gaps, nearly all with a common root cause; three were reproduced as real executions, and a patch closing them was re-checked with all failure gates enabled, after which a follow-up patch closed a defect the re-check itself exposed. Systematic extensions of the failure model (crash-restart, stale reads, two attempts) each found the windows they were designed to probe. Second, a single probe of the production payment sandbox exposed a response-shape divergence that makes an entire recovery ladder unreachable against the live API. The emulator-based audit could not detect it, because code and emulator share the same misreading: a correlated-oracle failure. Third, the companion study's central finding replicates across seven models from two vendors: contract structure, not language, governs what LLMs specify reliably. The replication concerns the ordering of contracts and the failure taxonomy, not the absolute level: only the strongest models reached the corpus ceiling, and the harder task restores discriminating power the benchmark had lost.

2026-07-06T13:39:00Z 25 pages, 3 figures, 5 tables. Artifacts and reference models at https://github.com/jdubray/SysMoBench-1 Jean-Jacques Dubray http://arxiv.org/abs/2607.07728v1 2026-07-06T09:47:59Z

This paper presents a deterministic algorithm for resolving ambiguity in parse trees using a global mutable context. The proposed method applies a tournament-style selection process to competing derivations at each non-terminal, systematically discarding alternatives whose non-terminal subtrees are not selected by the contextual decision mechanism. Unlike approaches that rely on post-processing, the algorithm maintains semantic state throughout incremental Abstract Syntax Tree (AST) building, allowing earlier decisions to influence the resolution of future ambiguities. This context-aware strategy enables consistent and procedural disambiguation after parsing. It features syntactic disambiguation based on a document environment instead of relying on ad-hoc rules, thus able to model complex relationships between previous constructs and the different derivations for a same non-terminal.

2026-07-06T09:47:59Z Preprint. 9 pages, 2 figures Alejandro Luis Vaz Mayato http://arxiv.org/abs/2602.24279v2 2026-07-06T09:45:39Z

We show that every two-way deterministic finite automaton (2DFA) that solves one-way liveness on height h has Omega(h^2) states. This implies a quadratic lower bound for converting one-way nondeterministic finite automata to 2DFAs, which asymptotically matches Chrobak's well-known lower bound for this conversion on unary languages. In contrast to Chrobak's simple proof, which relies on a 2DFA's inability to differentiate between any two sufficiently distant locations in a unary input, our argument can be applied to inputs over any alphabet and is structured around a main lemma that is general enough to potentially be reused elsewhere.

2026-02-27T18:50:33Z 17 pages, 4 figures, conference version presented at SOFSEM 2026, this version to be submitted to DMTCS's special issue for SOFSEM 2026 Kehinde Adeogun Christos Kapoutsis http://arxiv.org/abs/2209.10517v19 2026-07-06T08:56:56Z

In this paper, we define the notion of a {\em probabilistic $ω$-pushdown automaton} and study its model-checking problem against $ω$-probabilistic computational tree logic ($ω$-PCTL) and its bounded version from a computational complexity perspective. Specifically, we obtain the following important new results: (1) We first discuss the expressiveness of the logics PCTL, PCTL$^*$, $ω$-${\rm PCTL}$, and $ω$-${\rm PCTL}^*$ and study how Büchi conditions of probabilistic $ω$-pushdown systems influence $ω$-PCTL formulas. We then investigate the model-checking problem for {\em stateless probabilistic $ω$-pushdown system ($ω$-pBPA)} against $ω$-PCTL (as defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}). By constructing $ω$-PCTL formulas that encode the {\em Post Correspondence Problem}, we show that this model-checking problem is generally undecidable. (2) We then study under which conditions there exists an algorithm for model-checking {\it stateless probabilistic $ω$-pushdown systems} against $ω$-PCTL-like logic. In particular, we show that the model-checking problem for {\it stateless probabilistic $ω$-pushdown systems} against $ω$-{\it bounded probabilistic computational tree logic} ($ω$-bPCTL) is decidable and $\mathit{NP}$-hard. Currently, there is no known lower bound for this problem that is better than ours. (3) Finally, we investigate an upper bound for the model-checking problem for {\em stateless probabilistic $ω$-pushdown systems} against $ω$-bounded probabilistic computational tree logic ($ω$-bPCTL). We propose a potential approach to solving it by establishing a conditional upper bound and analyze the challenges of this method.

2022-09-21T17:33:48Z [v19] Incorporating answers to anonymous readers' all comments; comments are welcome Deren Lin Tianrong Lin