https://arxiv.org/api/cAJ0GOr8OQQPsmV79vdimoW/Pmg 2026-03-28T09:12:06Z 5879 120 15 http://arxiv.org/abs/1901.00175v5 2026-02-13T14:02:00Z

Metric Temporal Logic (MTL) is a popular formalism to specify temporal patterns with timing constraints over the behavior of cyber-physical systems with application areas ranging in property-based testing, robotics, optimization, and learning. This paper focuses on the unified construction of sequential networks from MTL specifications over discrete and dense time behaviors to provide an efficient and scalable online monitoring framework. Our core technique, future temporal marking, utilizes interval-based symbolic representations of future discrete and dense timelines. Building upon this, we develop efficient update and output functions for sequential network nodes for timed temporal operations. Finally, we extensively test and compare our proposed technique with existing approaches and runtime verification tools. Results highlight the performance and scalability advantages of our monitoring approach and sequential networks.

2019-01-01T16:23:24Z Logical Methods in Computer Science, Volume 22, Issue 1 (February 16, 2026) lmcs:14053 Dogan Ulus 10.46298/lmcs-22(1:12)2026 http://arxiv.org/abs/2602.12468v1 2026-02-12T22:55:05Z

Diffusion language models offer a promising alternative to autoregressive models due to their global, non-causal generation process, but their continuous latent dynamics make discrete constraints -- e.g., the output should be a JSON file that matches a given schema -- difficult to impose. We introduce a training-free guidance method for steering continuous diffusion language models to satisfy formal syntactic constraints expressed using regular expressions. Our approach constructs an analytic score estimating the probability that a latent state decodes to a valid string accepted by a given regular expression, and uses its gradient to guide sampling, without training auxiliary classifiers. The denoising process targets the base model conditioned on syntactic validity. We implement our method in Diffinity on top of the PLAID diffusion model and evaluate it on 180 regular-expression constraints over JSON and natural-language benchmarks. Diffinity achieves 68-96\% constraint satisfaction while incurring only a small perplexity cost relative to unconstrained sampling, outperforming autoregressive constrained decoding in both constraint satisfaction and output quality.

2026-02-12T22:55:05Z Jinwoo Kim Taylor Berg-Kirkpatrick Loris D'Antoni http://arxiv.org/abs/2602.12436v1 2026-02-12T21:48:41Z

Barrier certificates, a form of state invariants, provide an automated approach to the verification of the safety of dynamical systems. Similarly to barrier certificates, recent works explore the notion of closure certificates, a form of transition invariants, to verify dynamical systems against $ω$-regular properties including safety. A closure certificate, defined over state pairs of a dynamical system, is a real-valued function whose zero superlevel set characterizes an inductive transition invariant of the system. The search for such a certificate can be effectively automated by assuming it to be within a specific template class, e.g. a polynomial of a fixed degree, and then using optimization techniques such as sum-of-squares (SOS) programming to find it. Unfortunately, one may not be able to find such a certificate for a fixed template. In such a case, one must change the template, e.g. increase the degree of the polynomial. In this paper, we consider a notion of multiple closure certificates dubbed interpolation-inspired closure certificates. An interpolation-inspired closure certificate consists of a set of functions which jointly over-approximate a transition invariant by first considering one-step transitions, then two, and so on until a transition invariant is obtained. The advantage of interpolation-inspired closure certificates is that they allow us to prove properties even when a single function for a fixed template cannot be found using standard approaches. We present SOS programming and a scenario program to find these sets of functions and demonstrate the effectiveness of our proposed method to verify persistence and general $ω$-regular specifications in some case studies.

2026-02-12T21:48:41Z Mohammed Adib Oumer Vishnu Murali Majid Zamani http://arxiv.org/abs/2602.12058v1 2026-02-12T15:19:18Z

Model checking in TLA+ provides strong correctness guarantees, yet practitioners continue to face significant challenges in interpreting counterexamples, understanding large state-transition graphs, and repairing faulty models. These difficulties stem from the limited explainability of raw model-checker output and the substantial manual effort required to trace violations back to source specifications. Although the TLA+ Toolbox includes a state diagram viewer, it offers only a static, fully expanded graph without folding, color highlighting, or semantic explanations, which limits its scalability and interpretability. We present ModelWisdom, an interactive environment that uses visualization and large language models to make TLA+ model checking more interpretable and actionable. ModelWisdom offers: (i) Model Visualization, with colorized violation highlighting, click-through links from transitions to TLA+ code, and mapping between violating states and broken properties; (ii) Graph Optimization, including tree-based structuring and node/edge folding to manage large models; (iii) Model Digest, which summarizes and explains subgraphs via large language models (LLMs) and performs preprocessing and partial explanations; and (iv) Model Repair, which extracts error information and supports iterative debugging. Together, these capabilities turn raw model-checker output into an interactive, explainable workflow, improving understanding and reducing debugging effort for nontrivial TLA+ specifications. The website to ModelWisdom is available: https://model-wisdom.pages.dev. A demonstrative video can be found at https://www.youtube.com/watch?v=plyZo30VShA.

2026-02-12T15:19:18Z Accepted by FM 2026 Research Track (Tool) Zhiyong Chen Jialun Cao Chang Xu Shing-Chi Cheung http://arxiv.org/abs/2602.11949v1 2026-02-12T13:45:28Z

Modern property graph database query languages such as Cypher, PGQL, GSQL, and the standard GQL draw inspiration from the formalism of regular path queries (RPQs). In order to output walks explicitly, they depart from the classical and well-studied homomorphism semantics. However, it then becomes difficult to present results to users because RPQs may match infinitely many walks. The aforementioned languages use ad-hoc criteria to select a finite subset of those matches. For instance, Cypher uses trail semantics, discarding walks with repeated edges; PGQL and GSQL use shortest walk semantics, retaining only the walks of minimal length among all matched walks; and GQL allows users to choose from several semantics. Even though there is academic research on these semantics, it focuses almost exclusively on evaluation efficiency. In an attempt to better understand, choose and design RPQ semantics, we present a framework to categorize and compare them according to other criteria. We formalize several possible properties, pertaining to the study of RPQ semantics seen as mathematical functions mapping a database and a query to a finite set of walks. We show that some properties are mutually exclusive, or cannot be met. We also give several new RPQ semantics as examples. Some of them may provide ideas for the design of new semantics for future graph database query languages.

2026-02-12T13:45:28Z 30 pages, 1 figure Victor Marsault Antoine Meyer 10.4230/LIPIcs.ICDT.2026.6 http://arxiv.org/abs/2602.00036v2 2026-02-11T14:46:05Z

Large Language Models (LLMs), trained solely on massive text data, have achieved high performance on the Winograd Schema Challenge (WSC), a benchmark proposed to measure commonsense knowledge and reasoning abilities about the real world. This suggests that the language produced by humanity describes a significant portion of the world with considerable nuance. In this study, we attempt to harness the high expressive power of language within cellular automata. Specifically, we express cell states and rules in natural language and delegate their updates to an LLM. Through this approach, cellular automata can transcend the constraints of merely numerical states and fixed rules, providing us with a richer platform for simulation. Here, we propose LOGOS-CA (Language Oriented Grid Of Statements - Cellular Automaton) as a natural framework to achieve this and examine its capabilities. We confirmed that LOGOS-CA successfully performs simple forest fire simulations and also serves as an intriguing subject for investigation from an Artificial Life (ALife) perspective. In this paper, we report the results of these experiments and discuss directions for future research using LOGOS-CA.

2026-01-18T20:11:05Z Keishu Utimula http://arxiv.org/abs/2602.12300v1 2026-02-11T10:36:18Z

We propose a new method, that we coined the ``morphism-trick'', to integrate custom implementations of vector-Jacobian products in automatic differentiation softwares, applicable to a wide range of semiring-based computations. Our approach leads to efficient and semiring-agnostic implementations of the backward pass of dynamic programming algorithms. For the particular case of finite-state methods, we introduce an algorithm that computes and differentiates the $\oplus$-sum of all paths' weight of a finite-state automaton. Results show that, with minimal effort from the user, our novel library allows computing the gradient of a function w.r.t. to the weights of a finite state automaton orders of magnitude faster than state-of-the-art automatic differentiation systems. Implementations are made available via an open-source library distributed under a permissive license.

2026-02-11T10:36:18Z Lucas Ondel Yang LISN, CNRS Tina Raissi RWTH Aachen Martin Kocour FIT / BUT, BUT Pablo Riera ICC Caio Corro LinkMedia, INSA Rennes, IRISA http://arxiv.org/abs/2602.10654v1 2026-02-11T08:59:15Z

The JEDEC committee defines various domain-specific DRAM standards. These standards feature increasingly complex and evolving protocol specifications, which are detailed in timing diagrams and command tables. Understanding these protocols is becoming progressively challenging as new features and complex device hierarchies are difficult to comprehend without an expressive model. While each JEDEC standard features a simplified state machine, this state machine fails to reflect the parallel operation of memory banks. In this paper, we present an evolved modeling approach based on timed Petri nets and Python. This model provides a more accurate representation of DRAM protocols, making them easier to understand and directly executable, which enables the evaluation of interesting metrics and the verification of controller RTL models, DRAM logic and memory simulators.

2026-02-11T08:59:15Z Derek Christ Thomas Zimmermann Philippe Barbie Dmitri Saberi Yao Yin Matthias Jung http://arxiv.org/abs/2509.22912v2 2026-02-11T01:08:16Z

We introduce multi-head finite-state dimension, a generalization of finite-state dimension in which a group of finite-state agents (the heads) with oblivious, one-way movement rules, each reporting only one symbol at a time, enable their leader to bet on subsequent symbols in an infinite data stream. In aggregate, such a scheme constitutes an $h$-head finite state gambler whose maximum achievable growth rate of capital in this task, quantified using betting strategies called gales, determines the multi-head finite-state dimension of the sequence. The 1-head case is equivalent to finite-state dimension as defined by Dai, Lathrop, Lutz and Mayordomo (2004). In our main theorem, we prove a strict hierarchy as the number of heads increases, giving an explicit sequence family that separates, for each positive integer $h$, the earning power of $h$-head finite-state gamblers from that of $(h+1)$-head finite-state gamblers. We prove that multi-head finite-state dimension is stable under finite unions but that the corresponding quantity for any fixed number $h>1$ of heads--the $h$-head finite-state predimension--lacks this stability property.

2025-09-26T20:40:46Z Xiang Huang Xiaoyuan Li Jack H. Lutz Neil Lutz http://arxiv.org/abs/2602.10320v1 2026-02-10T21:58:45Z

Global protocols specify distributed, message-passing protocols from a birds-eye view, and are used as a specification for synthesizing local implementations. Implementability asks whether a given global protocol admits a distributed implementation. We present the first comprehensive investigation of global protocol implementability modulo network architectures. We propose a set of network-parametric Coherence Conditions, and exhibit sufficient assumptions under which it precisely characterizes implementability. We further reduce these assumptions to a minimal set of operational axioms describing insert and remove behavior of individual message buffers. Our reduction immediately establishes that five commonly studied asynchronous network architectures, namely peer-to-peer FIFO, mailbox, senderbox, monobox and bag, are instances of our network-parametric result. We use our characterization to derive optimal complexity results for implementability modulo networks, relationships between classes of implementable global protocols, and symbolic algorithms for deciding implementability modulo networks. We implement the latter in the first network-parametric tool Sprout(A), and show that it achieves network generality without sacrificing performance and modularity.

2026-02-10T21:58:45Z Elaine Li Thomas Wies http://arxiv.org/abs/2602.10036v1 2026-02-10T17:59:24Z

The theory of finite automata concerns itself with words in a free monoid together with concatenation and without further structure. There are, however, important applications which use alphabets which are structured in some sense. We introduce automata over a particular type of structured data, namely an alphabet which is given as a (finite or infinite) directed graph. This constrains concatenation: two strings may only be concatenated if the end vertex of the first is equal to the start vertex of the second. We develop the beginnings of an automata theory for languages on graph alphabets. We show that they admit a Kleene theorem, relating rational and regular languages, and a Myhill-Nerode theorem, stating that languages are regular iff they have finite prefix or, equivalently, suffix quotient. We present determinization and minimization algorithms, but we also exhibit that regular languages are not stable by complementation. Finally, we mention how these structures could be generalized to presimplicial alphabets, where languages are no more freely generated.

2026-02-10T17:59:24Z Hugo Bazille Uli Fahrenberg http://arxiv.org/abs/2509.22489v2 2026-02-10T17:47:53Z

We present a passive automata learning algorithm that can extract automata from recurrent networks with very large or even infinite alphabets. Our method combines overapproximations from the field of Abstract Interpretation and passive automata learning from the field of Grammatical Inference. We evaluate our algorithm by first comparing it with the state-of-the-art automata extraction algorithm from Recurrent Neural Networks trained on Tomita grammars. Then, we extend these experiments to regular languages with infinite alphabets, which we propose as a novel benchmark.

2025-09-26T15:35:20Z Corrected version of the work published in OVERLAY 2025, 7th International Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis Jaouhar Slimi Tristan Le Gall Augustin Lemesle http://arxiv.org/abs/2601.15214v2 2026-02-10T17:11:02Z

We consider (logical) reasoning for regular expressions with lookahead (REwLA). In this paper, we give an axiomatic characterization for both the (match-)language equivalence and the largest substitution-closed equivalence that is sound for the (match-)language equivalence. To achieve this, we introduce a variant of propositional dynamic logic (PDL) on finite linear orders, extended with two operators: the restriction to the identity relation and the restriction to its complement. Our main contribution is a sound and complete Hilbert-style finite axiomatization for the logic, which captures the equivalences of REwLA. Using the extended operators, the completeness is established via a reduction into an identity-free variant of PDL on finite strict linear orders. Moreover, the extended PDL has the same computational complexity as REwLA.

2026-01-21T17:39:30Z Long version of a paper accepted at FoSSaCS 2026 Yoshiki Nakamura http://arxiv.org/abs/2602.09896v1 2026-02-10T15:34:25Z

An $ω$-regular language is Eve-positional if, in all games with this language as objective, the existential player can play optimally without keeping any information from the previous moves. This notion plays a crucial role in verification, automata theory and synthesis. Casares and Ohlmann recently gave several characterizations of Eve-positionallity of $ω$-regular languages. For this, they introduce the notion $\varepsilon$-complete parity automaton and show (among other results) that an $ω$-regular language is Eve-positional if and only if it can be recognized by some $\varepsilon$-completion of a deterministic parity automaton. Colcombet and Idir extended on their work, and obtained a more direct semantic characterization of Eve-positionality. We introduce a new formalism that characterizes the Eve-positional languages, consisting in a restriction of non-deterministic Büchi automata. This allows us to complete a missing implication in Casares and Ohlmann's work. We then use this formalism to describe a determinization procedure for non-deterministic Büchi automaton recognizing such languages, with size blow-up at most factorial. We also show that this construction is, in a suitable sense, optimal.

2026-02-10T15:34:25Z Olivier Idir http://arxiv.org/abs/2509.17992v2 2026-02-10T14:41:11Z

This paper addresses the lifting problem for the Černý conjecture: namely, whether the validity of the conjecture for a quotient automaton can always be transferred (or "lifted") to the original automaton. Although a complete solution remains open, we show that it is sufficient to verify the Černý conjecture for three specific subclasses of reset automata: radical, simple, and quasi-simple. Our approach relies on establishing a Galois connection between the lattices of congruences and ideals of the transition monoid. This connection not only serves as the main tool in our proofs but also provides a systematic method for computing the radical ideal and for deriving structural insights about these classes. In particular, we show that for every simple or quasi-simple automaton $\mathcal{A}$, the transition monoid $\text{M}(\mathcal{A})$ possesses a unique ideal covering the minimal ideal of constant (reset) maps; a result of similar flavor holds for the class of radical automata.

2025-09-22T16:34:49Z 24 pages Emanuele Rodaro Riccardo Venturi