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.

TBA.

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.

Résumé à venir.

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.

Résumé à venir.

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.

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.

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.

Résumé à venir.

Résumé à venir.