https://arxiv.org/api/nhxsj8u6ni9lWlRYPdH6FoLBUM0 2026-03-26T11:04:35Z 5878 105 15 http://arxiv.org/abs/2602.15435v1 2026-02-17T08:57:31Z

The zone abstraction, widely adopted for its notable practical efficiency, is the de facto standard in the verification of Timed Automata (TA). Nonetheless, region-based abstractions have been shown to outperform zones in specific subclasses of TA. To complement and support mature zone-based tools, we introduce TARZAN, a C++ region-based verification library for TA. The algorithms implemented in TARZAN use a novel region abstraction that tracks the order in which clocks become unbounded. This additional ordering induces a finer partitioning of the state space, enabling backward algorithms to avoid the combinatorial explosion associated with enumerating all ordered partitions of unbounded clocks, when computing immediate delay predecessor regions. We validate TARZAN by comparing forward reachability results against the state-of-the-art tools Uppaal and TChecker. The experiments confirm that zones excel when TA have large constants and strict guards. In contrast, TARZAN exhibits superior performance on closed TA and TA with punctual guards. Finally, we demonstrate the efficacy of our backward algorithms, establishing a foundation for region-based analysis in domains like Timed Games, where backward exploration is essential.

2026-02-17T08:57:31Z Andrea Manini Matteo Rossi Pierluigi San Pietro http://arxiv.org/abs/2102.02777v4 2026-02-17T04:21:47Z

I propose a class of non-positional numeral systems where numbers are represented by Dyck words, with the systems arising from a recursive extension of prime factorization. After describing two proper subsets of the Dyck language capable of uniquely representing all natural numbers and a superset of the rational numbers respectively, I consider "Dyck-complete" languages, in which every member of the Dyck language represents a number. I conclude by suggesting possible research directions.

2021-02-04T17:56:44Z Minor corrections and clarifications after the previous major revision. No changes to results or references. Ancillary files added Ralph L. Childress http://arxiv.org/abs/2602.13351v2 2026-02-17T03:19:21Z

Finite automata (FA) are a fundamental computational abstraction that is widely used in practice for various tasks in computer science, linguistics, biology, electrical engineering, and artificial intelligence. Given an input word, an FA maps the word to a result, in the simple case "accept" or "reject", but in general to one of a finite set of results. A question that then arises is: why? Another question is: how can we modify the input word so that it is no longer accepted? One may think that the automaton itself is an adequate explanation of its behaviour, but automata can be very complex and difficult to make sense of directly. In this work, we investigate how to explain the behaviour of an FA on an input word in terms of the word's characters. In particular, we are interested in minimal explanations: what is the minimal set of input characters that explains the result, and what are the minimal changes needed to alter the result? In this paper, we propose an efficient method to determine all minimal explanations for the behaviour of an FA on a particular word. This allows us to give unbiased explanations about which input features are responsible for the result. Experiments show that our approach scales well, even when the underlying problem is challenging.

2026-02-12T23:58:56Z Jaime Cuartas Granada Alexey Ignatiev Peter J. Stuckey http://arxiv.org/abs/2602.10991v2 2026-02-16T14:12:51Z

While prior work established a verifier-based polynomial-time framework for NP, explicit deterministic machines for concrete NP-complete problems have remained elusive. In this paper, we construct fully specified deterministic Turing Machines (DTMs) for \textsc{SAT} and \textsc{Subset-Sum} within an improved NP verifier simulation framework. A key contribution of this work is the development of a functional implementation that bridges the gap between theoretical proofs and executable software. Our improved feasible-graph construction yields a genuine reduction in the asymptotic polynomial degree, while optimized edge-extension mechanisms significantly improve practical execution speed. We show that these machines generate valid witnesses, extending the framework to deterministic \textsc{FNP} computation without increasing complexity. The complete Python implementation behaves in accordance with the predicted polynomial-time bounds, and the source code along with sample instances are available in a public online repository.

2026-02-11T16:17:36Z Reference implementation available at: https://github.com/changryeol-hub/poly-np-sim The repository and manuscript may receive minor corrections and polishing updates after submission; these do not affect the theoretical results or polynomial complexity bounds Changryeol Lee http://arxiv.org/abs/2602.14748v1 2026-02-16T13:47:18Z

For a fixed regular language $L$, the enumeration of $L$-infixes is the following task: we are given an input word $w = a_1 \cdots a_n$ and we must enumerate the infixes of $w$ that belong to $L$, i.e., the pairs $i \leq j$ such that $a_i \cdots a_j \in L$. We are interested in dynamic enumeration of $L$-infixes, where we must additionally support letter substitution updates on $w$ (e.g., "replace the $i$-th letter of $w$ by a letter $a$"). Each update changes the set of infixes to enumerate, and resets the enumeration state. We study for which regular languages $L$ we can perform dynamic enumeration of $L$-infixes in constant delay (i.e., the next infix is always produced in constant time) and constant additional memory throughout the enumeration, while supporting each update in constant time. We show that, for languages $L$ with a neutral letter, if the language $L$ belongs to the class ZG and is extensible (i.e., if $u \in L$ and $u$ is a factor of $v$ then $v \in L$), then dynamic enumeration of $L$-infixes can be achieved with a simple algorithm that ensures constant-time updates and constant delay, but not constant additional memory. Our main contribution is then to show an algorithm that additionally uses only constant additional memory, and applies to a more general class of semi-extensible ZG languages for which we give several equivalent characterizations. We further discuss whether our results can be generalized to larger language classes and show some (conditional) lower bounds.

2026-02-16T13:47:18Z 34 pages, 1 figure. Submitted Antoine Amarilli Sven Dziadek Luc Segoufin http://arxiv.org/abs/2602.14722v1 2026-02-16T13:08:22Z

The intersection of two context-free languages is not generally context-free, but no geometric criterion has characterized when it remains so. The crossing gap (max(i'-i, j'-j) for two crossing push-pop arcs) is the natural candidate. We refute this: we exhibit CFLs whose intersection is CFL despite unbounded-gap crossings. The governing quantity is the inner segment measure: for crossing arcs inducing a decomposition w = P1 P2 P3 P4, it is max(|P2|,|P3|), the length of the longer inner segment between interleaved crossing endpoints. We prove a dichotomy for this measure: bounded inner segments imply context-freeness via a finite buffer construction; growing inner segments with pump-sensitive linkages imply non-context-freeness. The inner segment concept applies to all CFL intersections; the strictness of the resulting characterization depends on the language class. For block-counting CFLs (languages requiring equality among designated pairs of block lengths), the dichotomy is complete: the intersection is CFL if and only if the combined arcs are jointly well-nested. For general CFLs, the CFL direction is unconditional; the non-CFL direction requires pump-sensitive linkages whose necessity is the main open problem, reducing the general CFL intersection problem to a specific property of pump-sensitive decompositions.

2026-02-16T13:08:22Z 44 pages, 4 figures, 1 table Jorge Miguel Silva http://arxiv.org/abs/2207.13062v4 2026-02-15T21:52:57Z

It is well-known that the spacetime diagrams of some cellular automata have a fractal structure: for instance Pascal's triangle modulo 2 generates a Sierpinski triangle. It has been shown that such patterns can occur when the alphabet is endowed with the structure of an Abelian group, provided the cellular automaton is a morphism with respect to this structure and the initial configuration has finite support. The spacetime diagram then has a property related to k-automaticity. We show that these conditions can be relaxed: the Abelian group can be a commutative monoid, the initial configuration can be k-automatic, and the spacetime diagrams still exhibit the same regularity.

2022-07-26T17:34:12Z 33 pages, 13 figures Vincent Nesme http://arxiv.org/abs/2003.04728v6 2026-02-15T18:28:34Z

In this paper, we investigate the module-checking problem of pushdown multi-agent systems (PMS) against ATL and ATL* specifications. We establish that for ATL, module checking of PMS is 2EXPTIME-complete, which is the same complexity as pushdown module-checking for CTL. On the other hand, we show that ATL* module-checking of PMS turns out to be 4EXPTIME-complete, hence exponentially harder than both CTL* pushdown module-checking and ATL* model-checking of PMS. Our result for ATL* provides a rare example of a natural decision problem that is elementary yet but with a complexity that is higher than triply exponential-time.

2020-03-07T13:42:10Z Logical Methods in Computer Science, Volume 22, Issue 1 (February 17, 2026) lmcs:8458 Laura Bozzelli Aniello Murano Adriano Peron 10.46298/lmcs-22(1:13)2026 http://arxiv.org/abs/2509.19632v3 2026-02-15T04:29:40Z

The Harder-Narasimhan theory provides a canonical filtration of a vector bundle on a projective curve whose successive quotients are semistable with strictly decreasing slopes. In this article, we present the formalization of Harder-Narasimhan theory in the proof assistant Lean 4 with Mathlib. This formalization is based on a recent approach of Harder-Narasimhan theory by Chen and Jeannin, which reinterprets the theory in order-theoretic terms and avoids the classical dependence on algebraic geometry. As an application, we formalize the uniqueness of coprimary filtration of a finitely generated module over a noetherian ring, and the existence of the Jordan-Hölder filtration of a semistable Harder-Narasimhan game. Code available at: https://github.com/YijunYuan/HarderNarasimhan

2025-09-23T22:45:49Z 31 pages Yijun Yuan http://arxiv.org/abs/2602.13100v1 2026-02-13T17:05:30Z

We introduce the task of out-of-order membership to a formal language L, where the letters of a word w are revealed one by one in an adversarial order. The length |w| is known in advance, but the content of w is streamed as pairs (i, w[i]), received exactly once for each position i, in arbitrary order. We study efficient algorithms for this task when L is regular, seeking tight complexity bounds as a function of |w| for a fixed target language. Most of our results apply to an algebraically defined variant dubbed out-of-order evaluation: this problem is defined for a fixed finite monoid or semigroup S, and our goal is to compute the ordered product of the streamed elements of w. We show that, for any fixed regular language or finite semigroup, both problems can be solved in constant time per streamed symbol and in linear space. However, the precise space complexity strongly depends on the algebraic structure of the target language or evaluation semigroup. Our main contributions are therefore to show (deterministic) space complexity characterizations, which we do for out-of-order evaluation of monoids and semigroups. For monoids, we establish a trichotomy: the space complexity is either Θ(1), Θ(log n), or Θ(n), where n = |w|. More specifically, the problem admits a constant-space solution for commutative monoids, while all non-commutative monoids require Ω(log n) space. We further identify a class of monoids admitting an O(log n)-space algorithm, and show that all remaining monoids require Ω(n) space. For general semigroups, the situation is more intricate. We characterize a class of semigroups admitting constant-space algorithms for out-of-order evaluation, and show that semigroups outside this class require at least Ω(log n) space.

2026-02-13T17:05:30Z Antoine Amarilli Sebastien Labbe Charles Paperman http://arxiv.org/abs/2603.02238v1 2026-02-13T14:49:27Z

Length generalization is a key property of a learning algorithm that enables it to make correct predictions on inputs of any length, given finite training data. To provide such a guarantee, one needs to be able to compute a length generalization bound, beyond which the model is guaranteed to generalize. This paper concerns the open problem of the computability of such generalization bounds for CRASP, a class of languages which is closely linked to transformers. A positive partial result was recently shown by Chen et al. for CRASP with only one layer and, under some restrictions, also with two layers. We provide complete answers to the above open problem. Our main result is the non-existence of computable length generalization bounds for CRASP (already with two layers) and hence for transformers. To complement this, we provide a computable bound for the positive fragment of CRASP, which we show equivalent to fixed-precision transformers. For both positive CRASP and fixed-precision transformers, we show that the length complexity is exponential, and prove optimality of the bounds.

2026-02-13T14:49:27Z Andy Yang Pascal Bergsträßer Georg Zetzsche David Chiang Anthony W. Lin 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