Papers

Patterns are words with terminals and variables. The language of a pattern is the set of words obtained by uniformly substituting all variables with words that contain only terminals. In their original definition, patterns only allow for multiple distinct occurrences of some variables to be related by the equality relation, represented by using the same variable multiple times. In an extended notion, called relational patterns and relational pattern languages, variables may be related by arbitrary other relations, achieved by using regular patterns and relating individual variables independently from the patterns structure separately. We extend the ongoing investigation of the main decision problems for patterns (namely, the equivalence problem, the inclusion problem, and the membership problem) to relational pattern languages under a wide range of relevant individual relations, providing a comprehensive foundation in all three research directions.

We give a self-contained pair-automaton proof of the exact compress-with-another threshold of the corrected Figure 3 family from a recent survey of open problems in synchronizing automata. For every $p \geq 3$, the automaton has $n = 3p$ states and $\mu(q_0) = 4p = 4n/3$. The word $(ba)^p(ab)^p$ attains this value. Two entrance potentials and an excluded region yield the lower bound, with the endpoint exception at $p = 3$ treated explicitly. A separate reset construction proves $\operatorname{rt}(A_p) \leq 3p^2 + 4p - 1$ for every parameter. Reproducible computations verify the transition and entrance identities; the all-parameter results follow from the explicit proofs.

We introduce recurrent incidence automata (RIAs), a new automaton model motivated by a decomposition of certain two-stack visibly pushdown computations. The decomposition separates vertex-local finite-state computations from recurrent one-stack interfaces connecting consecutive vertices. The construction is motivated by a two-stack visibly pushdown encoding of arbitrary ordered graphs whose strings admit a unique factorization into center-foldable vertex-local factors and whose auxiliary stack is empty at every factor boundary. Folding each factor into a sequence of pair symbols yields a local interface transformation. An RIA consists of a finite-state unit that computes these transformations and a recurrent layer that composes them across consecutive factors. Rather than manipulating an internal pushdown store, RIAs externalize long-range stack memory into recurrent interfaces between local computations. We show that nondeterministic RIA languages are closed under union, intersection, concatenation, Kleene-*, and reversal. Deterministic RIAs are closed under Boolean operations, although emptiness remains undecidable.

The universality index corresponding to a word is the largest integer k such that every word of length k over the given alphabet occurs in it as a subsequence. Relative to languages this notion can be investigated with respect to both existential and universal quantifiers, with the former corresponding to the existence of a word in the language with universality index at least k, while the latter considers the index across all words that the language contains. In this work we study the existential (exists-universality) and universal (forall-universality) subsequence universality (as introduced in [Adamson et al., ISAAC 2023]) for binary languages consisting of all words with a fixed number of letters a, letters b, and subsequences ab. We prove that both exists- and forall-universality admit exact arithmetic characterizations for these languages. Extending the above notions, we end the paper by initiating the analysis of the probability of a fixed word occurring as subsequence of the words in such a language. To this end, we prove that, for every fixed pattern word w and an error tolerance, given as input the subsequence counts describing a language, the ratio of words in the language having the pattern w as a subsequence admits an additive approximation scheme that is polynomial-time in the binary encoding of the input counts.

It is well known that the pumping lemma for regular languages over finite alphabets does not extend to infinite alphabets. Instead, the generalized version of the pumping lemma for infinite alphabets states that the pumped patterns need not be identical, but only equivalent up to a finite-order permutation of the alphabet. This generalized variant of the pumping lemma involves two parameters: the length of the pumped pattern and an upper bound on the order of the permutation. We improve the known permutation-order bounds from factorial to tight bounds governed by Landau's function. We also show that, if the pumping length is sufficiently large, then permutations of order at most two always suffice. Our main structural result concerns the one-register case: every one-register automaton satisfies the classical pumping lemma, with no alphabet permutation. We prove a quadratic upper bound on the pumping length and give a matching quadratic lower bound up to constant factors. The same classical pumping phenomenon is shown for hierarchical register automata. Finally, we prove that, in general, deciding whether a quasi-regular language is pumpable for given constants is undecidable, while the minimal classical pumping length is computable for non-guessing one-register automata.

Motivated by educational applications, we study the problem of computing all corrections that transform a finite automaton into one recognizing a given regular language L. We show that for deterministic finite automata the set of all corrections can be finitely characterized as a regular tree language. The construction is based on a tree encoding of all deterministic finite automata recognizing L, which is extended to correction trees that make individual corrections and their induced edit-operations explicit. Leveraging the closure properties of regular tree languages, we introduce so-called filters for selecting corrections satisfying didactic constraints, enabling the derivation of individualized feedback from student submissions.

A certificate is a window of bytes with an origin inside it: wherever the window occurs in a completely tokenizable input, the token covering the window's final byte begins at that origin. Decided from the token set alone, a certified position marks where work may soundly begin. This paper decides certification and reads its anchors forward, into cuts, edits and audits. Certification is decided two ways: online with a completeness cutoff for literal vocabularies, and offline through an armed-run verifier for arbitrary regular token sets. Either route, under a declared window budget, yields the anchor inventory, with a witness on each refusal. The consequences are theorems. Cutting an input at certified anchors and scanning the chunks independently reproduces the sequential segmentation, with no speculation and no fixup pass. A byte substitution that keeps the input tokenizable moves boundaries only strictly between the certified anchors witnessed in the unchanged bytes on either side of it. For tokens of length at most L, an edit at p moves no boundary at or below p - L + 1. A delimiter permits a sound cut before it exactly when it sits only token-initial, and one after it exactly when only token-final, so the embedded-delimiter failure is refused. Two instruments follow: the anchor-free span of a finite certified inventory, decided bounded or not with its exact supremum, three for the UTF-8 shape; and a differential auditor deciding whether two token sets place different boundaries on an input both tokenize, with witnesses. Every theorem carries an executable check. Every measurement is a named program's output or arithmetic on such outputs, each program shipped with the paper or pinned by commit in the library it studies; that library's threaded scanner splits the archived campaign corpus at certified anchors, its boundary stream byte-identical throughout.

We prove several conjectures from the On-Line Encyclopedia of Integer Sequences about the lower and upper Wythoff sequences and the Fibonacci word. Among them are two of Kimberling's three conjectures on the number of ways to write $n=\lfloor h\varphi\rfloor+\lfloor k\varphi^2\rfloor$ with $h,k\ge1$ (A259598): exactly one way if and only if $n+1=2F$ for a Fibonacci number $F\ge2$, and exactly two ways if and only if $n+1\ge7$ is a Lucas number. The third conjecture, that no way exists if and only if $n+1$ is a Fibonacci number, was proved earlier by Kawsumarng et al. We also observe that Kimberling's conjecture on the gaps of the sums of two distinct terms of A003622 and of their complement (A333308, A333309) follows, after a shift by $2$, from earlier Walnut results of Shallit and of Bosma et al. on A260317, and we re-verify it. Next, we prove Kimberling's five 2025 conjectures on the gaps between positions where the Fibonacci word and the "Lucas word" take prescribed values (A383423-A383427). Finally, we prove a conjecture of Mathar on A285383, and we point out that a conjecture of Schmidt on A003250 follows from theorems of Carlitz, Scoville and Vaughan (1973); we also confirm it with Walnut. Most proofs are decision procedures run in the free prover Walnut, and we supply the complete command file.

Large language models (LLMs) are increasingly deployed in safety-critical settings, yet their black-box nature makes it difficult to provide formal guaranties about their behavior. Existing verification approaches rely primarily on empirical probing and testing, leaving open the question of how to reason rigorously about general-purpose trans- former architectures. In this work, we establish a principled bridge between transformers and weighted automata, a classical model from formal language theory. This connection enables us to transfer verification tools from automata the- ory to the analysis of LLMs. Our contributions are twofold: First, we develop a formal correspondence between transformer architectures and weighted automata over reals, showing how distributional properties of LLMs can be captured within this framework. Second, we introduce an identity testing algorithm for weighted automata that provides a statis- tical method for distinguishing whether two stochastic models define the same distribution up to a tolerance threshold. This work provides the first formal bridge between modern neural se- quence models and classical automata theory, clarifying both the poten- tial and the computational challenges for rigorous LLM verification.

Finite Fibonacci words have recently been shown to contain exactly three net occurrences—occurrences of repeated factors whose one-letter left and right extensions are unique. This unexpectedly small constant raises a natural question: is it peculiar to the Fibonacci recurrence, or part of a broader morphic phenomenon? We study a family over the alphabet $\{0,1,\ldots,d-1\}$ determined by positive integers $e_0,\ldots,e_{d-1}$. For each letter $a$, let $L_a$ be the morphism that fixes $a$ and maps every other letter $b$ to $ab$; we consider the finite approximants $S_m=\mu^m(0)$ generated by $\mu=L_0^{e_0}\cdots L_{d-1}^{e_{d-1}}$. These words are the period-aligned finite approximants of the purely morphic regular epistandard family considered here. We prove a sharp dichotomy: for every $m\ge2$, $S_m$ has exactly three net occurrences when $e_{d-1}=1$, and exactly two when $e_{d-1}\ge2$; the initial approximant is also completely classified. The proof combines palindromic prefixes, return-word factorizations, and overlapping net-occurrence covers. As a consequence, when all exponents are equal to one—the standard $d$-bonacci case—every noninitial period-aligned finite approximant has exactly three net occurrences, placing the Fibonacci phenomenon in a wider epistandard framework.

Graphoid automata evaluate graphs by composing relations between words of states. We examine the equations that make this evaluation independent of the chosen graph expression, and what changes when relations are replaced by matrices over a commutative semiring. We prove that the classical graphoid equations are equivalent to the special commutative Frobenius equations together with the required symmetry laws. The known cospan and hypergraph presentations then describe equality of structural and labelled expressions, with the bone law deleting precisely the isolated internal vertices. We use established partition representations to compare this equality with equality of evaluated matrices. For any nonempty finite state set $Q$ and commutative semiring $K$, we give a uniform criterion for two structural expressions to have the same matrix. The criterion determines which isolated-vertex counts are distinguished and when a vanishing scalar makes matrices from different boundary partitions equal. For the canonical structure, the bone law holds precisely when $|Q|\cdot1_K=1_K$. Preserving all relational compositions is a separate requirement, equivalent to additive idempotency for $|Q|\geq2$. We then examine the characteristic matrices of the known relational structures on $Q$ given by disjoint unions of Abelian groups. Their Frobenius equations hold over every commutative semiring, whereas specialness depends on the order of each group and the bone law depends on the number of groups. These conditions specify which equations remain valid when weights are assigned to a graphoid automaton.

Answering a question of Madill and Rampersad, we give an example a of a $2$-automatic sequence whose abelian complexity is not $2$-regular.

This paper presents a construction of a small universal machine within the framework of Multi-set Reaction Systems. We encode the machine state using elements that represent registers and instruction labels, and we enforce sequential execution by ensuring that reaction chains for a given instruction can only activate after the corresponding label element appears. We implement a universal register machine with 8 registers and 23 instructions, showing that the priority-based model requires 87 distinct elements. The results demonstrate that multiset reaction systems are capable of simulating universal computation.

A binary word is a shuffle square if its positions can be partitioned into two identical subsequences. A finite word over $\{1,2\}$ is smooth if repeated finite run-length differentiation remains binary until the empty word is reached. This paper proves that every smooth binary word in which both letters have even multiplicity is a shuffle square once its length is at least $18$. There are exactly $34$ exceptions, all of length at most $16$. The infinite part of the proof is a parity-return atom induction: a smooth even-Parikh word factors uniquely into smooth parity atoms, and every such atom has length at most $8$. A finite, independently checkable certificate handles lengths $18$ through $40$. As a consequence, a nonempty prefix of the classical Kolakoski sequence is a shuffle square if and only if both symbols occur an even number of times and its length is not $4$ or $8$. There are infinitely many such prefixes. In fact, the entire infinite Kolakoski sequence can be partitioned into two identical infinite subsequences with monochromatic blocks of uniformly bounded length.

We address the problem of temporal causality and explainability for reactive systems, and, in this setting, study sufficient reasons and contrastive explanations. These two notions are well-known explainability measures in the context of neural networks. In this work, we unify these notions for reactive systems and formal specifications given in temporal logic, providing dedicated definitions for sufficient reasons and contrastive explanations. We then lift these definitions to temporal sufficient reasons and contrastive explanations, providing more general and symbolic representations of explainability. We analyze the complexity of both verifying and finding explanations of the different types, and we demonstrate our approach using a prototype implementation.

Integer reachability is NP-complete for vector addition systems with states (VASS), but becomes PSPACE-complete in the presence of transfer operations. We refine this complexity gap for single-transfer VASS by identifying structural features of transfers responsible for the increase in complexity. Each system induces a transfer graph whose vertices are counters and whose edges represent possible transfers. We classify its vertices as good or bad, according to the branching and cyclic structure of their reachable subgraphs. Let $b$ be the number of bad vertices. We show that every positive instance admits a polynomially verifiable certificate of size $|I|^{O(b+1)}$, where $|I|$ is the input size. Consequently, integer reachability for single-transfer VASS can be decided in nondeterministic time $|I|^{O(b+1)}$; in particular, it belongs to NP for every class with a bounded number of bad counters. Conversely, we show that bad counters provide sufficient structural power to encode space-bounded computation. For every transfer graph with $b$ bad vertices, we construct a single-transfer VASS that encodes the acceptance of a Turing machine using $b^{O(1)}$ tape cells. This yields PSPACE-hardness for every polynomial-time constructible family of transfer graphs containing linearly many bad vertices. Our results isolate the transfer patterns responsible for the complexity of integer reachability.

Constrained generation aims to sample from language models (LMs) conditioned on hard constraints. Existing constrained-generation techniques for nondeterministic finite automaton (NFA) constraints either distort the distribution or sacrifice efficiency. Theoretically, this task reduces to counting the length-$n$ sequences accepted by an NFA (#NFA), and the exact #NFA problem is #P-complete. Recent work has shown that #NFA admits a fully polynomial randomized approximation scheme (FPRAS). Inspired by this result, we propose NFA-LM, a polynomial-time engine for NFA-constrained generation with theoretical guarantees under mild assumptions. Experiments show that NFA-LM efficiently generates high-quality outputs with theoretically bounded approximation error.

We study one-dimensional binary cellular automata with a five-slot radius-two local rule of exact algebraic-normal-form degree two, acting on periodic rings of length n. We prove that every such rule is non-injective whenever 4 | n and n >= 8. The proof begins with the four-cell collapse, where the two extreme formal slots coincide. A structural classification of the resulting four-variable maps separates the 65,472 exactly quadratic rules into 63,456 rules with an immediate ring-four collision and 2,016 exceptional lifts. The latter split into layers of sizes 480 and 1,536. Their remaining finite obligations are represented by 136 parameter-region constructions and 768 per-lift records, respectively. Each certificate supplies differentiating closed walks of lengths 8 and 12 with a common pair-graph base vertex. Concatenation then gives lengths 8a + 12b, which are exactly the multiples of four from eight onward. The load-bearing finite certificate core therefore contains 904 = 136 + 768 independently replayable objects checked by standalone, non-searching programs. The complete checker CLIs additionally reconstruct expected populations and execute coverage, complement, and regression/guard checks; 904 is not a count of total checker operations. Periodic extension also yields full-shift non-injectivity; that consequence is used here only as a corollary.

Structural analysis is a core method in Petri Net (PN) research, offering a perspective complementary to state-space techniques while avoiding many of their limitations. It is well studied for classical PNs but far less for High-Level Petri Nets (HLPN). Symmetric Nets (SN), a common HLPN formalism, use compact annotations to encode behavioral symmetries, enabling the construction of a symbolic reachability graph (and a lumped Markov chain in stochastic SN) and the execution of symbolic discrete-event simulations. During the past two decades, structural techniques tailored to SN have been developed, notably supported by the SNexpression tool. This tool implements a formal calculus designed for the computation of symbolic structural relations, including, but not limited to, conflict relations and causal dependencies. Here, we focus on using this calculus to verify semi-automatically symbolic structural invariants, a task currently feasible only for certain restricted SN subclasses. We focus specifically on (semi)flows and briefly discuss an approach through which a flow generative family can be generated, at least theoretically. We further briefly outline a framework for the formal verification of a broader class of invariant properties. An extended formulation of the SN formalism is employed, which demonstrably satisfies the closure property with respect to fundamental functional operators. The core concepts are elucidated by means of representative examples throughout the exposition.

Asynchronous communication is a fundamental feature of modern distributed systems, where messages are emitted without requiring immediate synchronization with receivers. In process calculi, this behaviour is typically modelled by separating message emission from message consumption. At the same time, reversible computation has emerged as an important paradigm for analysing concurrent systems, enabling computations to be undone while preserving causal dependencies between actions. While reversible semantics have been extensively studied for synchronous process calculi such as CCS, their integration with asynchronous communication remains largely unexplored. In this paper we investigate the interaction between asynchrony and reversibility in the setting of CCS. We first introduce CCSa, an asynchronous variant of CCS in which output actions generate explicit message entities that can later be consumed by matching input actions. We then define rCCSa, a reversible extension of CCSa obtained by adapting the framework of Phillips and Ulidowski. In rCCSa, prefixes and messages are annotated with unique keys that record message emission and consumption events, allowing computations to be reversed while preserving causal dependencies. We show that the resulting reversible semantics satisfies causal consistency, ensuring that computations can be reversed exactly up to causal equivalence. The proof relies on the axiomatic framework for reversible computation proposed by Lanese et al.

We describe the formalization in Dafny of two computational models, Turing Machines and the Lambda Calculus. We present several application of the formalizations: machine proofs of termination for Turing machines, Dafny proofs for Church encodings, and a mechanized proof of the Church-Rosser theorem.

We study finite resources governing exact positive reconstruction in fixed-observation CFG and MCFG learning. For an explicit rigid CFG family we compute safe observation size, internal residual fragmentation, and characteristic-data cost exactly. The result is a two-point Pareto frontier: after compulsory rigidity witnesses are fixed, exact reconstruction reduces to connectivity inside observer fibers, and the variable part of every minimum characteristic sample is a spanning forest of complete bipartite fiber graphs. For bounded-fan-out MCFG reconstruction, pure transition fragmentation multiplies across children. An explicit fan-out-two family X_{k,r} therefore has exact characteristic-data costs 2r[1+r(k-1)] and 2rk^r under two comparable observers. An integral lattice invariant yields an affine-span lower bound and a unimodularity test. In the binary-index subfamily, unimodularity suffices for minimum-cardinality samples through ranks two and three but not rank four. Two distinct obstructions then appear: an order-independent laminar support conflict, and an order-sensitive occurrence-scheduling conflict. For disjoint child requirements, the exact scheduling threshold is the largest monochromatic run count in the doubled reduced slot-colour word; in the two-colour case this is an alternation threshold. Horn nonlocking and Cartesian locking certificates make these constraints explicit. Hierarchical reuse can trade parent-root exposure for local fan-out: for the natural critical-module library of the mixed rank-four shapes, the exact width–anchor frontiers are {(2,1)}, {(2,2),(3,1)}, and {(4,1)} for separated, nested, and crossing orders. Thus observation, fragmentation, exposure, arithmetic span, laminar compatibility, ordered scheduling, and hierarchical reuse are genuinely distinct finite resources.

The limit set of Conway's Game of Life collects the configurations that can still appear at arbitrarily late times: those admitting predecessors of every finite depth. Answering a question of Salo and Törmä (ICALP 2022), we prove that two fixed finite patterns can each occur in the limit set, yet can never be found together in a single configuration of it, at any relative position; equivalently, the spatial translation action on the limit set is not topologically transitive. Our method is to make a persistent marker force a periodic lane to grow in sufficiently deep predecessors, until two perpendicular lanes are forced to intersect and prescribe incompatible values at a common cell. The argument uses two computer-verified local implications.

Modern cloud applications are built from loosely-coupled microservices that coordinate through well-defined APIs to service user requests. A single API request often triggers multiple downstream API calls, some executed sequentially and others spawned asynchronously in parallel. To certify safe and secure inter-service interactions in such applications, security and compliance teams must enforce policies not only over nested call/return structure, but also over the parallel structure of an execution: which calls may run concurrently, how many parallel branches can be spawned, and what combination of branch outcomes are allowed. However, existing runtime enforcement mechanisms typically model executions as sequential or purely nested traces, and cannot capture the parallel structure introduced by asynchronous API calls. Furthermore, since application implementations may not be accessible to security and compliance teams, the policy enforcement mechanism should be decoupled from the service implementation. We introduce SafePar, a specification and monitoring framework for policies over concurrent microservice executions. A SafePar policy constrains both the order of API calls and their series-parallel structure. To support seamless deployments, each policy is compiled into a series-parallel visibly pushdown automaton, a new model of computation we propose in this work, that drives a distributed runtime monitor implemented on top of the servicemesh layer. Our technique is blackbox and non-invasive: it requires no access or changes to the service implementation. Our experiments show that SafePar enforces rich concurrency-aware policies while incurring only millisecond-scale latency overhead.

Diffusion language models (dLLMs) predict masked positions in arbitrary order, but their exact constrained decoders still encode constraints as sequential languages, whose state must track every unresolved dependency between positions. For relational constraints this encoding grows exponentially: for same-order copy, every finite automaton needs $4^k$ states, deterministic or nondeterministic, and every context-free grammar has size $2^{\Omega(k)}$, while the factor graph of the same relation has size $O(k)$ and a 16-entry peak table. We introduce FactorDLM, a training-free decoder that represents finite-domain relations as a factor graph and, at each denoising step, conditions the model's mean-field prediction on that graph exactly by variable elimination. Decoding cost then grows exponentially with the induced width of the constraint graph, which replaces automaton size as the governing parameter. Because a finite automaton is a chain-shaped factor graph, one compiler enforces syntax and nonlocal relations together: on JSON records with cross-field references, a schema automaton alone leaves references dangling, relational factors alone produce malformed JSON, and the combined plan is valid on both counts, including on records of variable length. Across nine relational benchmarks and three backbones, every output satisfies every declared constraint at 0.4-6.9% projection overhead, where unconstrained decoding is 0-79% valid, and compiled projection answers repeated queries 13.6x faster than CP-SAT with eight parallel workers. Because model-free rules solve three of five standard benchmarks, we construct benchmarks with exact chance and fixed-template floors, on which selecting among exact constrained samples beats greedy projection. Which encoding is cheaper, sequential state or direct factors, depends on the constraint and is computable before decoding begins.

This paper studies learning of shuffle ideals with membership queries as well as with contrastive queries—a form of membership query that reveals not only whether a selected word $w$ is in the target language or not, but also provides a most similar word $w'$ that belongs to the target language if %and only if $w$ does not. For both settings, it is shown that even some very simple classes of shuffle ideals cannot be learned efficiently. By contrast, we obtain positive learnability results for classes of shuffle ideals that meet certain structural conditions. In the case of membership queries, these structural conditions are related to the previously studied notion of universal words, and raise new questions in word combinatorics. In the case of contrastive queries, the structural conditions relate to partitioning sets of words that are listed in shortlex order.

Semantics for systems with names and data often depends on finitely many distinguished values. The theory of finitely supported structures treats this dependence through invariance under permutations fixing a finite context. We develop this approach to semantics over arbitrary permutation groups and arbitrary infinite sets of atoms. The central difficulty is that finitely supported predicate spaces need not be complete lattices. We prove that, for predicates valued in a complete lattice with trivial atom action, every monotone finitely supported transformer nevertheless has least and greatest fixed points. These lie in the complete lattice determined by the transformer's context and coincide with the fixed points of every compatible monotone ambient extension equivariant under its stabilizer. Support-transfer bounds track dependencies through semantic constructions, while uniform finiteness yields finite convergence. For Boolean predicates, $m$ context-stabilizer orbits on the carrier suffice for convergence after at most $m$ iterations, even when the supported predicate lattice is orbit-infinite. We apply these results to automata, operational and modal semantics, abstract interpretation, and resource rewriting. Ultrahomogeneous atom structures in finite relational signatures yield finite cell representations, illustrated by an authorization monitor. The resulting account separates semantic existence, finite convergence, and effective computation.

Every finite nonempty incomplete uniquely decipherable code with maximum word length $k$ has an uncompletable word of length at most $4k^2-3k$. The bound is independent of the number of codewords and their total length. Deleting a complete codeword cycle gives a finite path-counting identity; Kraft equality then supplies a short word of deficient compressed mass. Cyclic averaging and padding turn it into an uncompletable word. Conditional expectation makes the construction polynomial-time and also decides completeness. First-return words extend the bound to mortal families of nonnegative integer $n\times n$ matrices with joint spectral radius at most one, provided every strongly connected component has a vertex meeting every cycle. Such a family has a zero product of length at most $4n^2-3n$. A binary partial deterministic family with $2k-1$ states has shortest zero product of length $k^2+k-1$, establishing the optimal quadratic order. The bounds and the explicit-code algorithm, including its polynomial work bound, are proved in Lean.

We construct an explicit deterministic one-tape, two-symbol Turing machine with 120 working states whose blank-tape computation halts if and only if the Riemann hypothesis is false. The machine uses the same binary blank-tape model and state-counting convention as the widely cited 744-state Matiyasevich-O'Rear-Aaronson construction. The reduction from 744 to 120 working states removes 624 states, or 83.87%. Subject to independent end-to-end verification, our machine is a new state-count record for the Riemann hypothesis.

Well-structured transition systems (WSTS) provide a classical framework for the verification of infinite-state systems, but their probabilistic extensions lack a unified treatment of quantitative coverability: path-enumeration algorithms assume a finite branching degree, while alternative approximation schemes defer some computations, such as probabilities over a bounded horizon, to the model at hand. We introduce probabilistic well-structured transition systems (pWSTS), Markov chains over countable state sets whose underlying transition systems are WSTS, with no a priori assumption on the branching degree. This class encompasses any WSTS equipped with a Markov kernel, such as probabilistic vector addition systems (pVAS) and probabilistic lossy channel systems (pLCS). For an effective subclass, we solve the approximate quantitative coverability problem over bounded horizons, and over infinite horizons under decisiveness, requiring no probabilistic information beyond individual transition probabilities. We then identify a general source of decisiveness: every stochastically monotone pWSTS is decisive with respect to every upward-closed set. We finally instantiate the framework on multi-type Galton–Watson processes, a classical model of population dynamics whose offspring distributions may have infinite support. Under mild assumptions on the reproduction laws, these processes are effective pWSTS, and they are stochastically monotone, hence decisive. Approximate quantitative coverability is therefore computable for them over both horizons, with a proof that uses none of the traditional tools: neither generating functions nor any case distinction between regimes.