Journées Annuelles 2025 — Groupe de travail GT-Vérif

Reinforcement Learning (RL) has shown great potential in many domains, yet its application in safety-critical contexts requires stronger guarantees. This talk explores how formal verification can enhance the reliability of learning-based systems.

Stochastic dynamical systems are ubiquitous in autonomous systems and safety-critical engineering. To ensure the safety and reliability of these systems, we need to compute control policies that ensure the system behaves as intended. Due to stochastic and nondeterministic uncertainty, nonlinear dynamics over continuous spaces, and the temporal nature of common specifications, computing optimal policies is a real challenge. In this talk, I will discuss two approaches—abstractions and certificates—to synthesizing policies that, while not optimal, still satisfy specifications with a desired probability. I will show how these techniques lead to powerful constructive (model-based) and inductive (data-driven) approaches to synthesizing provably correct policies under uncertainty.

Timed-Arc Petri nets (TAPN) are a timed extension of Petri nets where tokens have their age and each arc is associated with a time interval restricting the ages of tokens available for transition firing. Additionally, a TAPN can also contain place invariants constraining the ages of tokens in places, inhibitor arcs preventing a transition from firing and transport arcs that preserve a token's age upon firing. This set of features, as much as it allows us to model complex systems, also often makes verification problems computationally hard or even undecidable. Moreover, in order to model real-life examples, additional stochastic aspects are often necessary to capture the desired behaviour. We suggest (to the best of our knowledge) the first stochastic semantics for TAPNs and design and implement the Statistical Model Checking (SMC) algorithms in the model checker TAPAAL. We argue for the semantic choices we made in the stochastic semantics and prove that the semantics is well-behaving. On a number of case studies we demonstrate the practical applicability of our modelling formalism and its SMC implementation.

The model checking of Petri nets is generally done by constructing reachability graphs. However, this approach overlooks a key aspect of the model: concurrency. Some works adopt concurrent step semantics, which allows a limited form of parallelism where concurrent events must start and terminate simultaneously; but this introduces its own set of challenges. Higher-dimensional automata (HDAs) were introduced by van Glabbeek (1991) in order to faithfully model concurrency, and the same author (2006) gives Petri net semantics in terms of HDAs. In a contribution to Petri Nets 2025, we have revised this translation, extended it to cover inhibitor arcs and other variants, and implemented a tool which implements the translation.

This talk is an introduction to B and Event-B formal languages, which have been created by Jean-Raymond Abrial. After a brief description of the B theory, we will focus on Event-B, the Rodin platform and the refinement and proof activities.

Railway systems are deemed critical in the sense that a failure can result in dramatic accidents. In this presentation we will explain how CLEARSY use formal methods and event-B to model, analyze and simulate these systems to help infrastructure managers to ensure safety on their lines.

Résumé à venir.

The problem of LTLf reactive synthesis is to build a transducer, whose output is based on a history of inputs, such that, for every infinite sequence of inputs, the conjoint evolution of the inputs and outputs has a prefix that satisfies a given LTLf specification. We describe the implementation of an LTLf synthesizer that outperforms existing tools on our benchmark suite. This is based on a new, direct translation from LTLf to a DFA represented as an array of Binary Decision Diagrams (MTBDDs) sharing their nodes. This MTBDD-based representation can be interpreted directly as a reachability game that is solved on-the-fly during its construction.

Safety and liveness are fundamental concepts in computer-aided verification. The safety-liveness classification of Boolean properties determines whether a given property can be falsified by observing a finite prefix of an infinite computation trace (always for safety, never for liveness). This talk extends the safety-liveness framework to quantitative properties, defined as arbitrary functions from infinite words to partially ordered domains. This framework will be instantiated with the classes of quantitative properties expressed by automata, which map infinite words to real numbers. Then, procedures for deciding whether a given automaton defines a safe or live property will be presented, together with a decomposition into safe and live automata.

Active automata learning infers automaton models of systems from behavioral observations, a technique successfully applied to a wide range of domains. Compositional approaches for concurrent systems have recently emerged. This talk presents a new framework allowing to take a significant step beyond available results and develop a general technique for compositional learning of a synchronizing parallel system with an unknown decomposition. The approach automatically refines the global alphabet into component alphabets while learning the component models. It is based on the development of a theoretical treatment of distributions of alphabets, i.e., sets of possibly overlapping component alphabets. This allows to characterize counter-examples that reveal inconsistencies with global observations, and show how to systematically update the distribution to restore consistency. Based on this theory, a compositional learning algorithm implementing these ideas is presented, where learning counterexamples precisely correspond to distribution counterexamples under well-defined conditions.Finally, some experiments are presented, showing that in more than 630 subject systems, the implementation of this new algorithm delivers orders of magnitude improvements (up to five orders) in membership queries and in systems with significant concurrency, it also achieves better scalability in the number of equivalence queries.

Stochastic zero-sum two-player games on finite graphs model reactive systems as interaction between the controller (Player 1) and the environment. The decisions of the environment are either antagonistic or stochastic, modeled by actions chosen by the opponent Player 2 or chosen randomly from a stochastic vertex. The value of a vertex is the supremum probability that Player 1 can produce a winning play starting from the vertex, no matter how the other player plays. Memory requirements for optimal strategies have been studied for both stochastic games and deterministic games (no stochastic vertices). In this work, we are interested in relating the memory requirement of stochastic games and deterministic games. For omega-regular objectives with a neutral letter, we first show that the memory requirements for winning almost-surely (with probability 1) in stochastic games is the same as in deterministic games. For strategies achieving the optimal value, we show that additional information about the Myhill-Nerode classes, that identifies the set of winning continuations, is also necessary. Conversely, we show that a product of the Myhill-Nerode automaton and the minimal memory structure for deterministic games suffices to play optimally in stochastic games. The talk is based on joint work in progress with Mickael Randour, Matéo Torrents and Pierre Vandenhove.

In this talk, we present a generic reduction procedure for active learning problems, inspired by a recent polynomial-time reduction of the exact learning problem for weighted automata over integers to that for weighted automata over rationals due to Buna-Marginean et al. We instantiate this to the concrete setting of learning weighted automata over number rings, that is, rings of integers in an algebraic number field. Our algorithm produces an automaton that has at most one more state than the minimal one. This is joint work with Quentin Aristote, Sam van Gool and Mahsa Shirmohammadi.

Résumé à venir.

Runtime Verification (RV) is gaining popularity due to its scala- bility and ability to analyse block-box systems. Monitoring is at the heart of RV; a logical formula ϕ, formalising some property of interest, is typically trans- lated into a monitor that checks whether the system under scrutiny satisfies ϕ during its execution. A logical formula ϕ is violation (resp. satisfaction) moni- torable iff there exists a monitor for ϕthat is both sound and complete w.r.t. its violation (resp. satisfaction) by a system; and ϕ is monitorable if it is violation or satisfaction monitorable. The monitorability problem is thus concerned with determining the largest subset of a logic L that is monitorable. Although this problem has been solved for expressive untimed logics, it remained open for timed logics, i.e., where formulae can express both the order of events and the quantity of time separating them. In our recent work, we solved the monitorability problem for T lin , a new expressive (linear-time) timed µ-calculus that we proposed. First, we show that T lin is strictly more expressive than MTL, the de facto timed extension of the well-known LTL. Second, we identify MT lin , the largest monitorable fragment of T lin and characterise its largest subsets of formulae that are violation mon- itorable, satisfaction monitorable, and complete monitorable (both satisfaction and violation monitorable). To the best of our knowledge, this is the first work that solves the monitorability problem for such an expressive timed logic. Our theoretical results are accompanied with compilers (i) from MTL to T lin and (ii) from MT lin formulae to monitors. Joint work with Giovanni Bernardi, Mohammed Foughali and Adrian Francalanza.

Contrary to the case of automata over finite words, omega-regular languages do not admit unique, minimal deterministic automata. Yet, not all hope is lost! In this talk I will introduce layered automata, a subclass of alternating parity automata, defined by syntactic conditions and extending deterministic ones. We show: - All layered automata are history-deterministic. - Each omega-regular language can be recognised by a unique minimal layered automaton, admitting a congruence-based description. - This minimal automaton is computable in polynomial time from a given layered automaton. This is a work in progress with Christof Löding and Igor Walukiewicz.

Psychological theories are rarely expressed using formal models, which limits their precision, testability, and integration with computational tools. In numerous fields, formal models play a crucial role in theory-building by increasing the precision of predictions, improving scientific reasoning, and facilitating collaboration. We propose an automata-based method to transform informal, verbal psychological theories into formal, analyzable models. This method uses a step-by-step refinement procedure, and the verification of properties to check that the system coincides with the modeled theory. We illustrate our method by providing a formalization of Lazarus and Folkman's well-known theory of stress (1984). Our approach is further validated through the identification of theoretical ambiguities, the formulation of new research questions prompted by the modeling process, and the formal verification of the resulting system via the so-called psychological model checking.

Automata learning has proved its usefulness in verification. Still, classical automata suffer from the drawback of having one transition per letter, which quickly becomes prohibitive when dealing with large alphabets (think Unicode and its 2^16 characters, or N if the letters correspond to timings). Symbolic automata allows for the handling of these large or infinite alphabets by having transitions described by predicates instead of a single letter. Learning this model has already been studied, especially in the active case, but the only previous algorithm for passive learning was mostly of theoretical interest. In this talk, I will present a novel algorithm that admits nice properties and that we think can be generalized even further than its current state.