https://arxiv.org/api/nhxsj8u6ni9lWlRYPdH6FoLBUM0 2026-07-22T19:48:37Z 6102 105 15 http://arxiv.org/abs/2606.26503v1 2026-06-25T01:22:10Z

In this paper, we formulate a scenario that an agent can never be sure that another agent can uniquely determine the state of a finite-state automaton based on its observations to the automaton at the current and any past time as the property of order-2 bygone-state opacity. Based on our concurrent composition and the classical observer, we derive a tool to verify this property in doubly exponential time. The interest of this result lies in that we extend inference of finite automata from a single agent to two ordered agents.

2026-06-25T01:22:10Z 21 pages, 9 figures Kuize Zhang http://arxiv.org/abs/2606.25979v1 2026-06-24T15:50:42Z

Runtime monitoring of quantitative signals faces a fundamental trade-off between volatility and over-aggregation: instantaneous observations are noisy, while long-run averages obscure local structure. Localisation measures such as discounted averages offer a principled middle ground, yet remain poorly understood in runtime verification. This paper studies discounted sums from a monitoring perspective, in both deterministic and stochastic settings. We formalize the discounted monitoring problem and show that exact, sound monitoring of discounted sums cannot be achieved with finite memory. To overcome this impossibility, we introduce $\varepsilon$-approximately sound monitoring, deriving explicit bounds on memory and observation requirements. We then extend the framework to stochastic processes via expected discounted sums, defining pointwise and uniform $(\varepsilon,δ)$-soundness notions, establishing statistical optimality, and proving impossibility beyond a precision threshold. We also formalize the resource complexity of deterministic discounted monitoring via affine register machines and prove a tight worst-case lower bound. Finally, we present a specification language for arithmetic expressions over multiple discounted sums with synchronous and asynchronous semantics, and evaluate our approach on practical scenarios including algorithmic fairness.

2026-06-24T15:50:42Z Filip Cano Thomas A. Henzinger Konstantin Kueffner N. Ege Saraç http://arxiv.org/abs/2606.25881v1 2026-06-24T14:25:12Z

The Sixteenth International Workshop on Non-Classical Models of Automata and Applications (NCMA 2026) was held in Rouen, France, on June 29 and 30, 2026, organized by the University of Rouen. The NCMA workshop series was established in 2009 as an annual event for researchers working on non-classical and classical models of automata, grammars or related devices. Such models are investigated both as theoretical models and as formal models for applications from different points of view.

2026-06-24T14:25:12Z EPTCS 446, 2026 Cezar Câmpeanu Martin Kutrib Sylvain Lombardy 10.4204/EPTCS.446 http://arxiv.org/abs/2607.00034v1 2026-06-24T11:49:30Z

The powerset construction is the classical determinisation procedure for nondeterministic finite automata. In the coalgebraic setting, this construction has been generalised to structured coalgebras, which are coalgebras equipped with extra data. For stochastic Moore machines over the distribution monad, a type of structured coalgebra, the determinisation construction induces a semantics assigning to each finite input word a distribution on the current output. This semantics is appropriate when only the current output matters, but it is too coarse for settings in which intermediate observations must also be taken into account, as is typical for agents solving POMDPs in control theory and reinforcement learning. In these contexts, agents need to condition on all realised observations, not just the final one, so to better plan for the future. This has been addressed from a category theoretic perspective through a procedure called ``unifilarisation'', which (in our context) takes a stochastic Mealy machine and produces a machine whose states are priors over the original state space and whose transitions are given by Bayesian filtering. Here we show that unifilarisation is an instance of coalgebraic determinisation. We work with Mealy machines over monads equipped with extra structure generalising the notion of the support of a distribution. We show that in this setting, unifilarisation arises from the general determinisation procedure. We then compare the resulting final coalgebra semantics with the Moore-style one. Instead of assigning only a distribution on current outputs to each finite input word, it yields causal stochastic behaviours, that is, families mapping input words to distributions on output words compatible with the ``causality'' constraint that outputs cannot depend on future inputs.

2026-06-24T11:49:30Z Manuel Baltieri Nathaniel Virgo http://arxiv.org/abs/2606.27399v1 2026-06-24T10:59:35Z

Business Process Management (BPM) is concerned with the systematic design, execution, monitoring, and improvement of business processes. Formal grammars have emerged as a particularly fruitful formalism for BPM, offering generative, declarative, and analytical capabilities that are uniquely well-suited to process-oriented concerns. This paper presents a systematic literature review of 34 primary studies at the intersection of formal grammars and BPM. We identify seven research streams: (i) process grammars for organizational process design; (ii) process modeling languages evaluated as grammars under the Bunge-Wand-Weber ontological framework; (iii) production-rule grammars for process structural specification and variant management; (iv) attribute grammars for the declarative specification and distributed execution of workflows; (v) graph grammars for the transformation, generation, and semantic analysis of process models; (vi) grammatical inference for process mining and discovery; and (vii) process algebras as grammar-like compositional frameworks for behavioral specification and verification. For each stream, we synthesize contributions, formalisms employed, and limitations. The review reveals that formal grammars have influenced BPM across every lifecycle phase (from organizational design to formal verification and data-driven discovery) yet the seven streams have developed largely in parallel, without cross-stream synthesis. We identify five corpus-grounded open challenges and argue that a deeper, unified exploitation of grammatical theory holds significant promise for advancing the state of the art in BPM.

2026-06-24T10:59:35Z Milliam Maxime Zekeng Ndadji http://arxiv.org/abs/2512.02080v3 2026-06-24T10:23:11Z

The integration of Formal Verification tools with Large Language Models (LLMs) offers a path to scale software verification beyond manual workflows. However, current methods remain unreliable: without a solid theoretical footing, the refinement process acts as a black box that may oscillate, loop, or diverge. This work bridges this critical gap by developing an LLM-Verifier Convergence Theorem, providing the first formal framework with provable guarantees for termination in multi-stage verification pipelines. We model the interaction not as a generic loop, but as a sequential absorbing Markov Chain comprising four essential engineering stages: \texttt{CodeGen}, \texttt{Compilation}, \texttt{InvariantSynth}, and \texttt{SMTSolving}. We prove that for any non-zero stage success probability ($δ> 0$), the system reaches the \texttt{Verified} state almost surely. Furthermore, because of the sequential nature of the pipeline, we derive a precise latency bound of $\mathbb{E}[n] \leq 4/δ$. We stress-tested this prediction in an extensive empirical campaign comprising over 90,000 trials. The results match the theory with striking consistency: every run reached verification, and the empirical convergence factor clustered tightly around $C_f\approx 1.0$, confirming that the $4/δ$ bound accurately mirrors system behavior rather than serving as a loose buffer. Based on this data, we identify three distinct operating zones -- marginal, practical, and high-performance -- and propose a dynamic calibration strategy to handle parameter drift in real-world environments. Together, these contributions replace heuristic guesswork with a rigorous architectural foundation, enabling predictable resource planning and performance budgeting for safety-critical software.

2025-11-30T22:19:09Z 36 pages, 9 figures Pierre Dantas Lucas Cordeiro Youcheng Sun Waldir Junior http://arxiv.org/abs/2605.13076v3 2026-06-24T09:09:09Z

The LLM-based generation of machine-readable outputs such as JSON has attracted significant attention for integration with external systems. However, existing approaches cannot strictly enforce the maximum number of tokens to be generated, leading to infinite generation or truncated outputs that cause a system malfunction. To address this limitation, we propose TruncProof, a novel grammar-constrained generation method that enables LLMs to produce grammatically valid JSONs while adhering to a predefined token limit. By leveraging the properties of LL(1) parsers, TruncProof efficiently approximates the minimum number of tokens required to complete a grammatically valid output at each decoding step. Experiments on the Text-to-JSON instruction tasks demonstrate that TruncProof successfully generates syntactically correct outputs even under strict token constraints. Furthermore, we show that TruncProof can be effectively combined with advanced decoding strategies, resulting in outputs that are not only grammatically valid but also semantically accurate. The source code is public at https://github.com/Yosshi999/TruncProof

2026-05-13T06:49:08Z Main paper (8 pages). Accepted at the International Joint Conference on Neural Networks (IJCNN 2026) Yoshio Kato Shuhei Tarashima http://arxiv.org/abs/2606.25172v1 2026-06-23T21:04:37Z

A regular language is recognized by a finite monoid, but a locally checkable explanation of that recognition can have a nontrivial update geometry. We study exact bounded-arity annotations for regular word languages under one-symbol substitutions. The cost of an edit is the number of annotation cells that a canonical locally accepted representation must change, together with the corresponding bit movement and the number of local constraints that must be revalidated. For every morphism recognizing a regular language, the balanced product annotation gives constant locality, linear size, O(log n) edit stability, O(log n) revalidation, and constant access to the membership value. The matching lower bound proved here is restricted to product decompositions that expose an edit-active nontrivial group quotient as ordered product labels; in that setting one substitution changes every quotient label on an ancestor path. We also show that annotation-free bounded-window recognition is exactly strict locality, prove closure properties for a two-sided total decision variant, and formulate the remaining constant-stability boundary as a finite obstruction problem. The ancillary files include Lean, CP-SAT, and CUDA certificates, including a context-free interval-chart experiment.

2026-06-23T21:04:37Z 24 pages; ancillary files include a Lean 4 proof kernel, CP-SAT feasibility certificates, and CUDA source/certificates for finite obstruction experiments Faruk Alpay Baris Basaran http://arxiv.org/abs/2606.24880v1 2026-06-23T17:55:48Z

Markov jump linear systems (MJLSs) model dynamical phenomena subject to random switching among multiple linear modes, driven by an underlying Markov chain. Classical notions such as mean and mean-square stability characterize the long-term asymptotic behaviour of the first and second moments of an MJLS, but they can be overly conservative or even misleading when only a specific subset of initial conditions is of interest. We tackle this challenge through the lens of model checking, where reasoning about specific sets of initial conditions is intrinsic to the approach. We begin by formalizing probabilistic computation tree logic (PCTL) on MJLSs, enabling the specification of state-based temporal properties for these systems. Building on this foundation, we extend the logic to capture moment-based stability properties relative to a prescribed set of initial states. While we ultimately do not obtain a decision procedure for the entire base logic, the logical extensions can be handled -- albeit with some technical subtleties -- by exploiting linear-algebraic techniques.

2026-06-23T17:55:48Z Extended version of a paper to appear at QEST'26 containing proofs and additional details Lena Becker Holger Hermanns http://arxiv.org/abs/2606.22413v2 2026-06-23T13:24:02Z

Vibe coding -- accepting LLM-generated source from natural-language intent with minimal review -- is fast and may be adequate for low-criticality consumer software. But for safety-critical systems governed by DO-178C, IEC 61508, or ISO 26262, it offers no path to certification: large language models (LLMs) provide no formal correctness guarantees, and existing remedies target verification-aware languages (Dafny, Verus, Lean) that are scarce in pretraining data and absent from industrial toolchains. This paper closes the gap. We present Forge (Formal method Oriented Refinement loop for GEnerated code): a closed-loop pipeline that guides vibe coding through formal verification using established Model-Driven Engineering (MDE) infrastructure. Through vibe coding, we generate Java source code; our pipeline then extracts -- via model transformations -- formal artefacts in three different formalisms, each checked by a complementary verifier: deductive verification (Dafny), Communicating Sequential Processes (CSP) refinement via the Failures-Divergences Refinement checker (FDR4), and theorem proving using Z-Machines in Isabelle; every verification failure becomes a structured correction prompt that drives the next code-generation iteration. The LLM is the draft generator, the MDE chain is the discriminator, and the developer never has to read the formal models. Empirically, we find that the pipeline produces standards-relevant verification evidence for LLM-generated Java -- a step toward certification.

2026-06-21T10:01:45Z Ran Wei Le Zhu Haochi Wang Jim Woodcock Fang Yan Simon Foster Xiangyang Ji http://arxiv.org/abs/2606.24074v1 2026-06-23T02:38:14Z

Wang~\cite{Wang2026} introduced the Stochastic-Oracle Turing Machine (SOTM) framework and defined token complexity as the minimum expected cost of interacting with a stochastic oracle needed to attain a specified solution quality for a task. This paper develops an analogous notion for certifying the reliability of a stochastic oracle on a given domain. Certification token complexity is the minimum expected token cost required, with controlled error probability, to distinguish oracles that meet a target reliability level from those that fall below a lower reliability threshold. We construct an SPRT-based certification SOTM that queries the oracle, computes binary correctness scores, and stops when the accumulated log-likelihood evidence crosses a decision threshold. The SOTM halts almost surely, satisfies the desired two-sided error guarantee over the reliability regions to be certified, and yields an explicit upper bound on certification token complexity in terms of the reliability thresholds, the error bound, and the expected per-turn token cost. We then establish a matching information-theoretic lower bound: even with adaptive queries, every error-bounded certification SOTM must incur the same leading-order expected token cost as the SPRT-based construction as the prescribed error bound tends to zero. Together, these bounds characterize the leading-order certification token complexity in the small-error regime.

2026-06-23T02:38:14Z 21 pages, 0 figures Jie Wang http://arxiv.org/abs/2405.06043v2 2026-06-22T19:02:10Z

Algorithms which learn environments represented by automata in the past have had complexity scaling with the number of states in the automaton, which can be exponentially large even for automata recognizing regular expressions with a small description length. We thus formalize a compositional language that can construct automata as transformations between certain types of category, representable as string diagrams, which better reflects the description complexity of various automata. We define complexity constraints on this framework by having them operate on categories enriched over filtered sets, and using these constraints, we prove elementary results on the runtime and expressivity of a subset of these transformations which operate deterministically on finite state spaces. These string diagrams, or "string machines," are themselves morphisms in a category, so it is possible for string machines to create other string machines in runtime to model computations which take more than constant memory. We prove sufficient conditions for polynomial runtime guarantees on these, which can help develop complexity constraints on string machines which also encapsulate runtime complexity.

2024-05-09T18:28:37Z 14 pages, 1 figure Nur Cataltepe Vanessa Kosoy http://arxiv.org/abs/2606.05939v2 2026-06-22T15:22:36Z

Real-time systems require the careful handling of timing aspects in their models. For critical applications, this entails the use of time-aware formal methods. Currently, such formal methods only account for timing and communication layers, excluding functional aspects. Thus, they are intended to be used as a posteriori analysis methods, on systems that have already been developed. In contrast, methods such as Event-B have been designed to build systems incrementally using a correct-by-construction approach, but are not equipped with the ability to express timing aspects and constraints. We propose a non-intrusive, tool-supported embedding of time and clocks in Event-B inspired by the features and semantics of timed automata. This enables the design of complex real-time systems while benefiting from the entire ecosystem and tooling support of the method. Refinement is extended to also take time into account, making it possible to design complex systems gradually in a correct-by-construction manner while integrating timing aspects from the top level. The embedding and associated methodology are illustrated on a case study, showcasing both how timed Event-B models may be derived from timed automata, how the extended expressivity of first-order logic and set theory at the core of Event-B enables finer modelling, and how timed refinement may be used to establish complex timing properties.

2026-06-04T09:40:05Z This work was supported by ANR grant ANR-24-CE25-5742 (TAPAS project) Guillaume Dupont Jun Sun http://arxiv.org/abs/2510.08127v2 2026-06-22T08:56:09Z

We study the membership problem to context-free languages (CFLs) on probabilistic words, that specify for each position a probability distribution on the letters. Our task is to compute, given a probabilistic word, what is the probability that a word drawn according to the distribution belongs to the language $L$. This problem generalizes the problem of counting how many words of length $n$ belong to $L$, or of counting how many completions of a partial word belong to $L$. We show that this problem is in polynomial time for unambiguous context-free languages (uCFLs), but can be #P-hard already for unions of two linear uCFLs. More generally, we show that the problem is in polynomial time for so-called poly-slicewise-unambiguous languages, where given a length $n$ we can tractably compute an uCFL for the words of length $n$ in the language. This class includes some inherently ambiguous languages, and implies the tractability of bounded CFLs and of languages recognized by unambiguous polynomial-time counter automata. We then introduce classes of circuits from knowledge compilation which we use for tractable counting, and show that this covers the tractability of poly-slicewise-unambiguous languages and of some CFLs that are not poly-slicewise-unambiguous. Extending these circuits with negation further allows us to show tractability for the language of primitive words, and for the language of concatenations of two palindromes. We also show that, when the target language is given as input, our problem is intractable already when the language asks whether there is a factor that matches one partial word; however, it becomes tractable when the language is given as a $k$-ambiguous automaton for any fixed $k>0$. We finally show the conditional undecidability of the meta-problem that asks, given a CFG, whether the probabilistic membership problem for that CFG is tractable or #P-hard.

2025-10-09T12:13:34Z 44 pages. This is an extended version of the conference article, that contains more results Antoine Amarilli Mikaël Monet Paul Raphaël Sylvain Salvati http://arxiv.org/abs/1603.02966v4 2026-06-21T11:54:11Z

Let $M(A,I)$ be a free partially commutative monoid with involution and $G(A,I)$ its quotient group (for example, a right-angled Artin or Coxeter group). We show that for any system of word equations over $M(A,I)$ with recognizable constraints, the solution set - in $M(A,I)$ or in $G(A,I)$ - is an EDT0L language. It is given by an NFA $\mathcal{A}$ recognizing endomorphisms over some extended monoid. Furthermore, if the input size is $n$, then the automaton $\mathcal{A}$ can be constructed effectively by an NSPACE$(n\log n)$-transducer. As a consequence, both Satisfiability (whether the system admits a solution) and Finiteness (whether the solution set is infinite) are decidable in NSPACE$(n \log n)$. For a natural subclass of constraints, we conjecture that these problems are NP-complete.

2016-03-09T17:03:22Z 86 pages Volker Diekert Artur Jeż Manfred Kufleitner Alexander Thumm