https://arxiv.org/api/vUTCgJoWqXaA9UuWZG0xcLr0TqY 2026-03-24T11:32:36Z 5876 60 15 http://arxiv.org/abs/2501.12932v4 2026-03-04T11:42:34Z

Recently, a distributed middleware application called contract automata runtime environment (CARE) has been introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling, verification and testing of CARE. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool Uppaal, utilising exhaustive and statistical model checking techniques. Abstract tests are generated from the Uppaal models that are concretised for testing CARE. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and generating concrete tests from the abstract model, addressing the issues that have been identified and fixed.

2025-01-22T15:03:25Z Logical Methods in Computer Science, Volume 22, Issue 1 (March 5, 2026) lmcs:15129 Davide Basile 10.46298/lmcs-22(1:8)2026 http://arxiv.org/abs/2602.19477v3 2026-03-04T02:02:33Z

The sandpile automata of Bak, Tang, and Wiesenfeld (Phys. Rev. Lett., 1987) are a simple model for the diffusion of particles in space. A fundamental problem related to the complexity of the model is predicting its evolution in the parallel setting. Despite decades of effort, a classification of this problem for two-dimensional sandpile automata remains outstanding. Fungal automata were recently proposed by Goles et al. (Phys. Lett. A, 2020) as a spin-off of the model in which diffusion occurs either in horizontal $(H)$ or vertical $(V)$ directions according to a so-called update scheme. Goles et al. proved that the prediction problem for this model with the update scheme $H^4V^4$ is $\textbf{P}$-complete. This result was subsequently improved by Modanese and Worsch (Algorithmica, 2024), who showed the problem is $\textbf{P}$-complete also for the simpler updatenscheme $HV$. In this work, we fill in the gaps and prove that the prediction problem is $\textbf{P}$-complete for any update scheme that contains both $H$ and $V$ at least once.

2026-02-23T03:40:29Z Eric Goles Augusto Modanese Martín Ríos-Wilson Domingo Ruiz-Tala Thomas Worsch http://arxiv.org/abs/2603.02796v1 2026-03-03T09:35:02Z

Motivated by targeted drug delivery, we investigate the gathering of particles in the full tilt model of externally controlled motion planning: A set of particles is located at the tiles of a polyomino with all particles reacting uniformly to an external force by moving as far as possible in one of the four axis-parallel directions until they hit the boundary. The goal is to choose a sequence of directions that moves all particles to a common position. Our results include a polynomial-time algorithm for gathering in a completely filled polyomino as well as hardness reductions for approximating shortest gathering sequences and for determining whether the particles in a partially filled polyomino can be gathered. We pay special attention to the impact of restricted geometry, particularly polyominoes without holes. As corollaries, we make progress on an open question from [Balanza-Martinez et al., SODA 2020] by showing that deciding whether a given position can be occupied remains NP-hard in polyominoes without holes and provide initial results on the parameterized complexity of tilt problems. Our results build on a connection we establish between tilt models and the theory of synchronizing automata.

2026-03-03T09:35:02Z 30 pages, 13 figures. Full version of an extended abstract to appear in the proceedings of the 42nd International Symposium on Computational Geometry (SoCG 2026) Sándor P. Fekete Jonas Friemel Peter Kramer Jan-Marc Reinhardt Christian Rieck Christian Scheffer http://arxiv.org/abs/2508.20671v3 2026-03-02T17:14:05Z

We introduce an abstract measure___theoretic framework that serves as a tool to rigorously study stochastic iterative global optimization algorithms as a unified class. The framework is formulated in terms of probability kernels, which, via the Ionescu--Tulcea theorem, induce probability measures on the space of sequences of algorithm iterations, endowed with two intuitive properties. This framework answers the need for a general, implementation___independent formalism in the analysis of such algorithms, providing a starting point for formalizing global optimization results in proof-assistants. To illustrate the relevance of our tool, we show that common algorithms fit naturally in the framework, and we also use it to give a rigorous proof of a general consistency theorem for stochastic iterative global optimization algorithms (Proposition 3 of (Malherbe, et al., 2017). This proof and the entire framework are formalized in the Lean proof assistant. This formalization both ensures the correctness of the definitions and proofs, and provides a basis for future machine-assisted formalizations in the field.

2025-08-28T11:23:10Z Gaëtan Serré ENS Paris Saclay, CB Argyris Kalogeratos CB, ENS Paris Saclay Nicolas Vayatis CB, ENS Paris Saclay http://arxiv.org/abs/2505.11199v3 2026-03-02T10:44:04Z

Counting properties (e.g. determining whether certain tokens occur more than other tokens in a given input text) have played a significant role in the study of expressiveness of transformers. In this paper, we provide a formal framework for investigating the counting power of transformers. We argue that all existing results demonstrate transformers' expressivity only for (semi-)linear counting properties, i.e., which are expressible as a boolean combination of linear inequalities. Our main result is that transformers can express counting properties that are highly nonlinear. More precisely, we prove that transformers can capture all semialgebraic counting properties, i.e., expressible as a boolean combination of arbitrary multivariate polynomials (of any degree). Among others, these generalize the counting properties that can be captured by C-RASP softmax transformers, which capture only linear counting properties. To complement this result, we exhibit a natural subclass of (softmax) transformers that completely characterizes semialgebraic counting properties. Through connections with the Hilbert's tenth problem, this expressivity of transformers also yields a new undecidability result for analyzing an extremely simple transformer model -- surprisingly with neither positional encodings (i.e. NoPE-transformers) nor masking. We also experimentally validate trainability of such counting properties.

2025-05-16T12:56:59Z Accepted for ICLR 2026 Marco Sälzer Chris Köcher Alexander Kozachinskiy Georg Zetzsche Anthony Widjaja Lin http://arxiv.org/abs/2603.00861v1 2026-03-01T01:34:15Z

Grudka, Karczewski, Kurzynski, Stempin, Wójcik and Wojcik (2025) constructed quantum channels with synchronizing words of length 3 for qutrits. We extend their result to arbitrarily long minimal synchronizing words, providing a contrast to Černý's conjecture for finite automata.

2026-03-01T01:34:15Z Quantum Communication, Networking and Computation (QCNC) 2026 Bjørn Kjos-Hanssen Swarnalakshmi Lakshmanan http://arxiv.org/abs/2501.08082v4 2026-02-28T11:58:39Z

This paper investigates complexity of the uniform membership problem for hyperedge replacement grammars in comparison with other mildly context-sensitive grammar formalisms. It turns out that the complexity of this problem depends on how one defines a hypergraph. There are two commonly used definitions in the field, which differ in whether repetitions of attachment nodes of a hyperedge are allowed in a hypergraph or not. We show that, in general, the problem under consideration is EXPTIME-complete, even for string-generating hyperedge replacement grammars, but it is NP-complete if repetitions are not allowed. We extend the developed proof techniques in order to prove a general meta-theorem: checking whether a given hyperedge replacement grammar generates a hypergraph satisfying a non-Parikh property is EXPTIME-hard. Non-Parikh properties are those that are not preimages of properties on Parikh vectors of hypergraphs. This includes any graph property relying significantly on structure of graphs, e.g. connectivity, Eulerianity, Hamiltonianity, acyclicity. A tight upper bound is established for EXPTIME-compatible properties via Filter Theorem.

2025-01-14T12:50:40Z Content is extended substantially as compared to the previous version (new meta-theorems are included here), and presentation is improved significantly Tikhon Pshenitsyn http://arxiv.org/abs/2308.08842v6 2026-02-28T06:07:55Z

Computing the reachability probability in infinite state probabilistic models has been the topic of numerous works. Here we introduce a new property called \emph{divergence} that when satisfied allows to compute reachability probabilities up to an arbitrary precision. One of the main interests of divergence is that this computation does not require the reachability problem, i.e., the possibility to reach target states from an initial state in a given model, to be decidable. Then we study the decidability of divergence for random walks and the probabilistic versions of Petri nets where the weights associated with transitions may also depend on the current state. This should be contrasted with most of the existing works that assume weights independent of the state. Such an extended framework is motivated by the modeling of real case studies. Moreover, we exhibit some subclasses of channel systems and pushdown automata that are divergent by construction, particularly suited for specifying open distributed systems and networks prone to performance collapsing where probabilities related to service requirements are needed.

2023-08-17T08:02:12Z 31 page. arXiv admin note: text overlap with arXiv:2305.19564 Alain Finkel Serge Haddad Lina Ye http://arxiv.org/abs/2510.26371v4 2026-02-27T20:22:58Z

Automata admitting at most one accepting run per structure, known as unambiguous automata, find applications in verification of reactive systems as they extend the class of deterministic automata whilst maintaining some of their desirable properties. In this paper, we generalise a classical construction of unambiguous automata from thin trees to thin coalgebras for analytic functors. This achieves two goals: extending the existing construction to a larger class of structures, and providing conceptual clarity and parametricity to the construction by formalising it in the coalgebraic framework. As part of the construction, we link automaton acceptance of languages of thin coalgebras to language recognition via so-called coherent algebras, which were previously introduced for studying thin coalgebras. This link also allows us to establish an automata-theoretic characterisation of languages recognised by finite coherent algebras.

2025-10-30T11:14:28Z Electronic Notes in Theoretical Informatics and Computer Science, Volume 5 - Proceedings of MFPS XLI (December 20, 2025) entics:16832 Anton Chernev Corina Cîrstea Helle Hvid Hansen Clemens Kupke 10.46298/entics.16832 http://arxiv.org/abs/2602.24279v1 2026-02-27T18:50:33Z

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

2026-02-27T18:50:33Z 18 pages, 4 figures, conference version presented at SOFSEM 2026, this version to be submitted to DMTCS's special issue for SOFSEM 2026 Kehinde Adeogun Christos Kapoutsis http://arxiv.org/abs/2509.22215v2 2026-02-27T14:46:53Z

Security verification of communication protocols in industrial and safety-critical systems is challenging because implementations are often proprietary, accessible only as black boxes, and too complex for manual modeling. As a result, existing security testing approaches usually depend on incomplete test suites and/or require labor-intensive modeling, limiting coverage, scalability, and trust. This paper addresses the problem of systematically verifying protocol security-properties without access to internal system models. We propose a flexible and scalable method for formal verification of communication protocols that combines active automata learning with model checking to enable rigorous security analysis of black-box protocol implementations. The key contributions include: (i) a method for augmenting learned protocol models with security-relevant propositions, (ii) a fully automated transformation pipeline from learned models to model-checking artifacts, (iii) reusable, generic security property templates that are instantiated in protocol-specific models, and (iv) empirical validation through case studies demonstrating applicability in different protocols and domains. The results show that the approach enables scalable and systematic discovery of security vulnerabilities in black-box systems while reducing modeling effort and improving automation compared with traditional verification workflows.

2025-09-26T11:29:53Z 26 pages, 9 figures, 4 tables, preprint submitted to Elsevier Computers & Security - Original abstract shortened to comply to the arXiv requirements Stefan Marksteiner Mikael Sjödin Marjan Sirjani http://arxiv.org/abs/2602.23927v1 2026-02-27T11:21:58Z

We present a multiparty session type (MST) framework with asynchronous mixed choice (MC). We propose a core construct for MC that allows transient inconsistencies in protocol state between distributed participants, but ensures all participants can always eventually reach a mutually consistent state. We prove the correctness of our system by establishing a progress property and an operational correspondence between global types and distributed local type projections. Based on our theory, we implement a practical toolchain for specifying and validating asynchronous MST protocols featuring MC, and programming compliant gen_statem processes in Erlang/OTP. We test our framework by using our toolchain to specify and reimplement part of the amqp_client of the RabbitMQ broker for Erlang.

2026-02-27T11:21:58Z Laura Bocchi Raymond Hu Adriana Laura Voinea Simon Thompson http://arxiv.org/abs/2602.23805v1 2026-02-27T08:44:19Z

Weighted automata over the nonnegative reals form a fundamental model for quantitative languages. We show that, up to scaling, this model collapses to probabilistic automata. Concretely, we prove that every weighted automaton whose transition matrix has spectral radius strictly less than one can be normalised, by a semantics-preserving rescaling of transition weights, into an equivalent locally stochastic probabilistic automaton. Thus, finite-mass weighted automata and probabilistic automata coincide up to normalisation. The construction is effective and relies on Perron-Frobenius theory. We further characterise probabilistic automata by stochastic regular expressions equipped with a geometrically weighted star. Beyond the finite-mass setting, we show that the behaviour of an arbitrary weighted automaton admits a decomposition into an exponential growth rate and a normalised probabilistic component, separating quantitative growth from stochastic structure.

2026-02-27T08:44:19Z Smayan Agarwal Aalok Thakkar http://arxiv.org/abs/2510.02524v2 2026-02-27T00:38:37Z

While large models achieve impressive results, their learning dynamics are far from understood. Many domains of interest, such as natural language syntax, coding languages, arithmetic problems, are captured by context-free grammars (CFGs). In this work, we extend prior work on neural language modeling of CFGs in a novel direction: how language modeling behaves with respect to CFG substructure, namely "subgrammars". We first define subgrammars, and prove a set of fundamental theorems regarding language modeling and subgrammars. We show that language modeling loss (or equivalently the Kullback-Leibler divergence) recurses linearly over its top-level subgrammars; applied recursively, the loss decomposes into losses for "irreducible" subgrammars. We also prove that the constant in this linear recurrence is a function of the expected recursion, a notion we introduce. We show that under additional assumptions, parametrized models learn subgrammars in parallel. Empirically, we confirm that small transformers learn subgrammars in parallel, unlike children, who first master simple substructures. We also briefly explore several other questions regarding subgrammars. We find that subgrammar pretraining can improve final performance, but only for tiny models relative to the grammar, while alignment analyses show that pretraining consistently lead to internal representations that better reflect the grammar's substructure in all cases; we also observe persistent difficulty with deeper recursion, a limitation that appears even of large language models.

2025-10-02T19:52:19Z Equal contribution by LYS and DM Laura Ying Schulz Daniel Mitropolsky Tomaso Poggio http://arxiv.org/abs/2410.18799v4 2026-02-26T16:54:09Z

We introduce a new class of automata (which we coin EU-automata) running on infininte trees of arbitrary (finite) arity. We develop and study several algorithms to perform classical operations (union, intersection, complement, projection, alternation removal) for those automata, and precisely characterise their complexities. We also develop algorithms for solving membership and emptiness for the languages of trees accepted by EU-automata. We then use EU-automata to obtain several algorithmic and expressiveness results for the temporal logic QCTL (which extends CTL with quantification over atomic propositions) and for MSO. On the one hand, we obtain decision procedures with optimal complexity for QCTL satisfiability and model checking; on the other hand, we obtain an algorithm for translating any QCTL formula with k quantifier alternations to formulas with at most one quantifier alternation, at the expense of a $(k + 1)$-exponential blow-up in the size of the formulas. Using the same techniques, we prove that any MSO formula can be translated into a formula with at most four quantifier alternations (and only one second-order-quantifier alternation), this time with a $(k + 2)$-exponential blow-up in the size of the formula.

2024-10-24T14:51:00Z François Laroussinie Nicolas Markey