Patricia Bouyer

CSL Conference 2025 Conference Paper

On the Probabilistic and Statistical Verification of Infinite Markov Chains (Invited Talk)

• Patricia Bouyer

The verification of infinite-state Markov chains is a challenging problem, even when those chains are described by structured high-level models. In 2007, Abdulla et al introduced the concept of decisiveness [Abdulla et al. , 2007], and showed that a natural approximation scheme could be applied to infinite Markov chains that are decisive. This was, up to our knowledge, the unique generic scheme that could be widely applied to (decisive) infinite Markov chains providing guarantees on the computed values (under some mild assumptions for effectiveness). On the other hand, statistical model-checking is a very efficient method that can be used for estimating probabilities in stochastic systems [Younes and Simmons, 2006; H. L. S. Younes et al. , 2010]. We explain in this talk that decisiveness is also a key concept that allows to apply such statistical methods to infinite Markov chains. While decisiveness is a crucial property, not all Markov chains are decisive, and it is therefore desirable to propose methods to analyze non-decisive Markov chains. Importance sampling [Kahn and Harris, 1951] is a method which has been proposed to improve efficiency of statistical model-checking, in particular for estimating probabilities of rare events in stochastic systems. The idea is to biase the original chain, and to estimate the probabilities in the biased chain; guarantees can sometimes be given, as studied for instance in [B. Barbot et al. , 2012]. In this talk, we will explain how we use the importance sampling idea to turn a non-decisive Markov chain into a biased decisive Markov chain, in which we can estimate probabilities (with guarantees). We apply the general approach to a class of probabilistic pushdown automata. Our algorithms have been implemented in the tool Cosmos [P. Ballarini et al. , 2015], and we discuss the methodology for experiments as well as our (partial) conclusions.

CSL Conference 2024 Conference Paper

From Local to Global Optimality in Concurrent Parity Games

• Benjamin Bordais
• Patricia Bouyer
• Stéphane Le Roux 0001

We study two-player games on finite graphs. Turn-based games have many nice properties, but concurrent games are harder to tame: e. g. turn-based stochastic parity games have positional optimal strategies, whereas even basic concurrent reachability games may fail to have optimal strategies. We study concurrent stochastic parity games, and identify a local structural condition that, when satisfied at each state, guarantees existence of positional optimal strategies for both players.

IJCAI Conference 2023 Conference Paper

Half-Positional Objectives Recognized by Deterministic Büchi Automata (Extended Abstract)

• Patricia Bouyer
• Antonio Casares
• Mickael Randour
• Pierre Vandenhove

In two-player zero-sum games on graphs, the protagonist tries to achieve an objective while the antagonist aims to prevent it. Objectives for which both players do not need to use memory to play optimally are well-understood and characterized both in finite and infinite graphs. Less is known about the larger class of half-positional objectives, i. e. , those for which the protagonist does not need memory (but for which the antagonist might). In particular, no characterization of half-positionality is known for the central class of ω-regular objectives. Here, we characterize objectives recognizable by deterministic Büchi automata (a class of ω-regular objectives) that are half-positional, both over finite and infinite graphs. This characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.

LAMAS&SR Workshop 2022 Workshop Paper

Characterizing Omega-Regularity through Finite-Memory Determinacy of Games on Infinite Graphs

• Patricia Bouyer
• Mickael Randour
• Pierre Vandenhove

I&C Journal 2022 Journal Article

Decisiveness of stochastic systems and its application to hybrid models

• Patricia Bouyer
• Thomas Brihaye
• Mickael Randour
• Cédric Rivière
• Pierre Vandenhove

In 2007, Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving the decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems.

CSL Conference 2022 Conference Paper

Finite-Memory Strategies in Two-Player Infinite Games

• Patricia Bouyer
• Stéphane Le Roux 0001
• Nathan Thomasset

We study infinite two-player win/lose games (A, B, W) where A, B are finite and W ⊆ (A×B)^ω. At each round Player 1 and Player 2 concurrently choose one action in A and B, respectively. Player 1 wins iff the generated sequence is in W. Each history h ∈ (A×B)^* induces a game (A, B, W_h) with W_h: = {ρ ∈ (A×B)^ω ∣ h ρ ∈ W}. We show the following: if W is in Δ⁰₂ (for the usual topology), if the inclusion relation induces a well partial order on the W_h’s, and if Player 1 has a winning strategy, then she has a finite-memory winning strategy. Our proof relies on inductive descriptions of set complexity, such as the Hausdorff difference hierarchy of the open sets. Examples in Σ⁰₂ and Π⁰₂ show some tightness of our result. Our result can be translated to games on finite graphs: e. g. finite-memory determinacy of multi-energy games is a direct corollary, whereas it does not follow from recent general results on finite memory strategies.

CSL Conference 2022 Conference Paper

Optimal Strategies in Concurrent Reachability Games

• Benjamin Bordais
• Patricia Bouyer
• Stéphane Le Roux 0001

We study two-player reachability games on finite graphs. At each state the interaction between the players is concurrent and there is a stochastic Nature. Players also play stochastically. The literature tells us that 1) Player 𝖡, who wants to avoid the target state, has a positional strategy that maximizes the probability to win (uniformly from every state) and 2) from every state, for every ε > 0, Player 𝖠 has a strategy that maximizes up to ε the probability to win. Our work is two-fold. First, we present a double-fixed-point procedure that says from which state Player 𝖠 has a strategy that maximizes (exactly) the probability to win. This is computable if Nature’s probability distributions are rational. We call these states maximizable. Moreover, we show that for every ε > 0, Player 𝖠 has a positional strategy that maximizes the probability to win, exactly from maximizable states and up to ε from sub-maximizable states. Second, we consider three-state games with one main state, one target, and one bin. We characterize the local interactions at the main state that guarantee the existence of an optimal Player 𝖠 strategy. In this case there is a positional one. It turns out that in many-state games, these local interactions also guarantee the existence of a uniform optimal Player 𝖠 strategy. In a way, these games are well-behaved by design of their elementary bricks, the local interactions. It is decidable whether a local interaction has this desirable property.

I&C Journal 2022 Journal Article

Synthesis in presence of dynamic links

• Béatrice Bérard
• Benedikt Bollig
• Patricia Bouyer
• Matthias Függer
• Nathalie Sznajder

We consider the problem of distributed synthesis: Given a distributed architecture and a specification, can we generate a distributed algorithm that satisfies the specification? While previous work focused on static architectures and fixed message sizes, we assume that the communication network changes dynamically and that processes piggy-pack previously received messages onto current messages. Specifically, we address two processes communicating in rounds over a dynamic link. Given a network model, i. e. , a set of link directions, an adversary picks, in each round, an arbitrary link from the network model. We show that the synthesis problem is decidable for a network model if and only if it does not contain the 'empty' link. For a more general setting allowing for sequences of links, the synthesis problem is decidable if and only if the number of consecutive empty links in all possible sequences is uniformly bounded from above.

GandALF Workshop 2020 Workshop Paper

Decisiveness of Stochastic Systems and its Application to Hybrid Models

• Patricia Bouyer
• Thomas Brihaye
• Mickael Randour
• Cédric Rivière
• Pierre Vandenhove

In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems. [ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).

ECAI Conference 2020 Conference Paper

Reasoning About Quality and Fuzziness of Strategic Behaviours

• Patricia Bouyer
• Orna Kupferman
• Nicolas Markey
• Bastien Maubert
• Aniello Murano
• Giuseppe Perelli

GandALF Workshop 2020 Workshop Paper

Synthesis in Presence of Dynamic Links

• Béatrice Bérard
• Benedikt Bollig
• Patricia Bouyer
• Matthias Függer
• Nathalie Sznajder

The problem of distributed synthesis is to automatically generate a distributed algorithm, given a target communication network and a specification of the algorithm's correct behavior. Previous work has focused on static networks with an a priori fixed message size. This approach has two shortcomings: Recent work in distributed computing is shifting towards dynamically changing communication networks rather than static ones, and an important class of distributed algorithms are so-called full-information protocols, where nodes piggy-pack previously received messages onto current messages. In this work, we consider the synthesis problem for a system of two nodes communicating in rounds over a dynamic link whose message size is not bounded. Given a network model, i. e. , a set of link directions, in each round of the execution, the adversary choses a link from the network model, restricted only by the specification, and delivers messages according to the current link's directions. Motivated by communication buses with direct acknowledge mechanisms, we further assume that nodes are aware of which messages have been delivered. We show that the synthesis problem is decidable for a network model if and only if it does not contain the empty link that dismisses both nodes' messages.

MFCS Conference 2019 Conference Paper

Nash Equilibria in Games over Graphs Equipped with a Communication Mechanism

• Patricia Bouyer
• Nathan Thomasset

We study pure Nash equilibria in infinite-duration games on graphs, with partial visibility of actions but communication (based on a graph) among the players. We show that a simple communication mechanism consisting in reporting the deviator when seeing it and propagating this information is sufficient for characterizing Nash equilibria. We propose an epistemic game construction, which conveniently records important information about the knowledge of the players. With this abstraction, we are able to characterize Nash equilibria which follow the simple communication pattern via winning strategies. We finally discuss the size of the construction, which would allow efficient algorithmic solutions to compute Nash equilibria in the original game.

TIME Conference 2019 Conference Paper

On the Computation of Nash Equilibria in Games on Graphs (Invited Talk)

• Patricia Bouyer

In this talk, I will show how one can characterize and compute Nash equilibria in multiplayer games played on graphs. I will present in particular a construction, called the suspect game construction, which allows to reduce the computation of Nash equilibria to the computation of winning strategies in a two-player zero-sum game.

IJCAI Conference 2019 Conference Paper

Reasoning about Quality and Fuzziness of Strategic Behaviours

• Patricia Bouyer
• Orna Kupferman
• Nicolas Markey
• Bastien Maubert
• Aniello Murano
• Giuseppe Perelli

We introduce and study SL[F], a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an SL[F] formula is a real value in [0, 1], reflecting ``how much'' or ``how well'' the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of SL[F] in quantitative reasoning about multi-agent systems, by showing how it can express concepts of stability in multi-agent systems, and how it generalises some fuzzy temporal logics. We also provide a model-checking algorithm for ourlogic, based on a quantitative extension of Quantified CTL*.

CSL Conference 2018 Conference Paper

Finite Bisimulations for Dynamical Systems with Overlapping Trajectories

• Béatrice Bérard
• Patricia Bouyer
• Vincent Jugé

Having a finite bisimulation is a good feature for a dynamical system, since it can lead to the decidability of the verification of reachability properties. We investigate a new class of o-minimal dynamical systems with very general flows, where the classical restrictions on trajectory intersections are partly lifted. We identify conditions, that we call Finite and Uniform Crossing: When Finite Crossing holds, the time-abstract bisimulation is computable and, under the stronger Uniform Crossing assumption, this bisimulation is finite and definable.

GandALF Workshop 2018 Workshop Paper

Multi-weighted Markov Decision Processes with Reachability Objectives

• Patricia Bouyer
• Mauricio González
• Nicolas Markey
• Mickael Randour

In this paper, we are interested in the synthesis of schedulers in double-weighted Markov decision processes, which satisfy both a percentile constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using a weighted reachability condition. This problem is inspired by the modelization of an electric-vehicle charging problem. We study the cartography of the problem, when one parameter varies, and show how a partial cartography can be obtained via two sequences of opimization problems. We discuss completeness and feasability of the method.

I&C Journal 2017 Journal Article

Nash equilibria in symmetric graph games with partial observation

• Patricia Bouyer
• Nicolas Markey
• Steen Vester

We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria for qualitative objectives in this game model.

Highlights Conference 2016 Conference Abstract

Decisive stochastic processes

• with Nathalie Bertrand
• Patricia Bouyer
• Pierre Carlier

In 2007, Abdulla et al. introduced the elegant concept of decisive Markov chain. Intuitively, decisiveness allows one to lift the good properties of finite Markov chains to infinite Markov chains. For instance, the approximate quantitative reachability problem can be solved for decisive Markov chains (enjoying reasonable effectiveness assumptions) including probabilistic lossy channel systems and probabilistic vector addition systems with states. In this paper, we extend the concept of decisiveness to more general stochastic processes. This extension is non trivial as we consider stochastic processes with a potentially continuous set of states and uncountable branching (common features of real-time stochastic processes). This allows us to obtain decidability results for both qualitative and quantitative verification problems on some classes of real-time stochastic processes, including generalized semi-Markov processes and stochastic timed automata. The results presented in this abstract are issued from a joint paper with Nathalie Bertrand, Patricia Bouyer and Pierre Carlier entitled Analysing decisive stochastic processes accepted to ICALP 2016.

MFCS Conference 2016 Invited Paper

Optimal Reachability in Weighted Timed Automata and Games

• Patricia Bouyer

This is an overview of the invited talk delivered at the 41st International Symposium on Mathematical Foundations of Computer Science (MFCS-2016).

GandALF Workshop 2016 Workshop Paper

Stochastic Equilibria under Imprecise Deviations in Terminal-Reward Concurrent Games

• Patricia Bouyer
• Nicolas Markey
• Daniel Stan

We study the existence of mixed-strategy equilibria in concurrent games played on graphs. While existence is guaranteed with safety objectives for each player, Nash equilibria need not exist when players are given arbitrary terminal-reward objectives, and their existence is undecidable with qualitative reachability objectives (and only three players). However, these results rely on the fact that the players can enforce infinite plays while trying to improve their payoffs. In this paper, we introduce a relaxed notion of equilibria, where deviations are imprecise. We prove that contrary to Nash equilibria, such (stationary) equilibria always exist, and we develop a PSPACE algorithm to compute one.

MFCS Conference 2016 Conference Paper

Stochastic Timed Games Revisited

• S. Akshay 0001
• Patricia Bouyer
• Shankara Narayanan Krishna
• Lakshmi Manasa
• Ashutosh Trivedi 0001

Stochastic timed games (STGs), introduced by Bouyer and Forejt, naturally generalize both continuous-time Markov chains and timed automata by providing a partition of the locations between those controlled by two players (Player Box and Player Diamond) with competing objectives and those governed by stochastic laws. Depending on the number of players - 2, 1, or 0 - subclasses of stochastic timed games are often classified as 2 1/2-player, 1 1/2-player, and 1/2-player games where the 1/2 symbolizes the presence of the stochastic "nature" player. For STGs with reachability objectives it is known that 1 1/2-player one-clock STGs are decidable for qualitative objectives, and that 2 1/2-player three-clock STGs are undecidable for quantitative reachability objectives. This paper further refines the gap in this decidability spectrum. We show that quantitative reachability objectives are already undecidable for 1 1/2 player four-clock STGs, and even under the time-bounded restriction for 2 1/2-player five-clock STGs. We also obtain a class of 1 1/2, 2 1/2 player STGs for which the quantitative reachability problem is decidable.

GandALF Workshop 2015 Workshop Paper

Average-energy games

• Patricia Bouyer
• Nicolas Markey
• Mickael Randour
• Kim G. Larsen
• Simon Laursen

Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in NP inter coNP and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.

TCS Journal 2015 Journal Article

Robust reachability in timed automata and games: A game-based approach

• Patricia Bouyer
• Nicolas Markey
• Ocan Sankur

Reachability checking is one of the most basic problems in verification. By solving this problem in a game, one can synthesize a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing “robust” strategies for ensuring reachability of a location in timed automata. By robust, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete. We also extend our algorithm, with the same complexity, to turn-based timed games, where the successor state is entirely determined by the environment in some locations.

I&C Journal 2014 Journal Article

Shrinking timed automata

• Ocan Sankur
• Patricia Bouyer
• Nicolas Markey

We define and study a new approach to the implementability of timed automata, where the semantics is perturbed by imprecisions and finite frequency of the hardware. In order to circumvent these effects, we introduce parametric shrinking of clock constraints, which corresponds to tightening these. We propose symbolic procedures to decide the existence of (and then compute) parameters under which the shrunk version of a given timed automaton is non-blocking and can time-abstract simulate the exact semantics. We then define an implementation semantics for timed automata with a digital clock and positive reaction times, and show that for shrinkable timed automata, non-blockingness and time-abstract simulation are preserved in implementation.

I&C Journal 2010 Journal Article

On the expressiveness of TPTL and MTL

• Patricia Bouyer
• Fabrice Chevalier
• Nicolas Markey

TPTL and MTL are two classical timed extensions of LTL. In this paper, we prove the 20-year-old conjecture that TPTL is strictly more expressive than MTL. But we show that, surprisingly, the TPTL formula proposed by Alur and Henzinger for witnessing this conjecture it can be expressed in MTL. More generally, we show that TPTL formulae using only modality F can be translated into MTL.

I&C Journal 2008 Journal Article

Timed Petri nets and timed automata: On the discriminating power of zeno sequences

• Patricia Bouyer
• Serge Haddad
• Pierre-Alain Reynier

Timed Petri nets and timed automata are two standard models for the analysis of real-time systems. We study in this paper their relationship, and prove in particular that they are incomparable with respect to language equivalence. In fact, we study the more general model of timed Petri nets with read-arcs (RA-TdPN), already introduced in [J. Srba, Timed-arc petri nets vs. networks of automata, in: Proceedings of the 26th International Conference Application and Theory of Petri Nets (ICATPN 05), Lecture Notes in Computer Science, vol. 3536, Springer, Berlin, 2005, pp. 385–402], which unifies both models of timed Petri nets and of timed automata, and prove that the coverability problem remains decidable for this model. Then, we establish numerous expressiveness results and prove that Zeno behaviours discriminate between several sub-classes of RA-TdPNs. This has surprising consequences on timed automata, for instance, on the power of non-deterministic clock resets.

TCS Journal 2004 Journal Article

Updatable timed automata

• Patricia Bouyer
• Catherine Dufourd
• Emmanuel Fleury
• Antoine Petit

We investigate extensions of Alur and Dill's timed automata, based on the possibility to update the clocks in a more elaborate way than simply reset them to zero. We call these automata updatable timed automata. They form an undecidable class of models, in the sense that emptiness checking is not decidable. However, using an extension of the region graph construction, we exhibit interesting decidable subclasses. In a surprising way, decidability depends on the nature of the clock constraints which are used, diagonal-free or not, whereas these constraints play identical roles in timed automata. We thus describe in a quite precise way the thin frontier between decidable and undecidable classes of updatable timed automata. We also study the expressive power of updatable timed automata. It turns out that any updatable automaton belonging to some decidable subclass can be effectively transformed into an equivalent timed automaton without updates but with silent transitions. The transformation suffers from an enormous combinatorics blow-up which seems unavoidable. Therefore, updatable timed automata appear to be a concise model for representing and analyzing large classes of timed systems.

I&C Journal 2003 Journal Article

An algebraic approach to data languages and timed languages

• Patricia Bouyer
• Antoine Petit
• Denis Thérien

Algebra offers an elegant and powerful approach to understand regular languages and finite automata. Such framework has been notoriously lacking for timed languages and timed automata. We introduce the notion of monoid recognizability for data languages, which includes timed languages as special case, in a way that respects the spirit of the classical situation. We study closure properties and hierarchies in this model and prove that emptiness is decidable under natural hypotheses. Our class of recognizable languages properly includes many families of deterministic timed languages that have been proposed until now, and the same holds for non-deterministic versions.

TCS Journal 2003 Journal Article

The power of reachability testing for timed automata

• Luca Aceto
• Patricia Bouyer
• Augusto Burgueño
• Kim G Larsen

The computational engine of the verification tool UPPAAL consists of a collection of efficient algorithms for the analysis of reachability properties of systems. Model-checking of properties other than plain reachability ones may currently be carried out in such a tool as follows. Given a property φ to model-check, the user must provide a test automaton T φ for it. This test automaton must be such that the original system S has the property expressed by φ precisely when none of the distinguished reject states of T φ can be reached in the synchronized parallel composition of S with T φ. This raises the question of which properties may be analysed by Uppaal in such a way. This paper gives an answer to this question by providing a complete characterization of the class of properties for which model-checking can be reduced to reachability testing in the sense outlined above. This result is obtained as a corollary of a stronger statement pertaining to the compositionality of the property language considered in this study. In particular, it is shown that our language is the least expressive compositional language that can express a simple safety property stating that no reject state can ever be reached. Finally, the property language characterizing the power of reachability testing is used to provide a definition of characteristic properties with respect to a timed version of the ready simulation preorder, for nodes of τ-free, deterministic timed automata.

MFCS Conference 2000 Conference Paper

Expressiveness of Updatable Timed Automata

• Patricia Bouyer
• Catherine Dufourd
• Emmanuel Fleury
• Antoine Petit 0001

Abstract Since their introduction by A lur and D ill, timed automata have been one of the most widely studied models for real-time systems. The syntactic extension of so-called updatable timed automata allows more powerful updates of clocks than the reset operation proposed in the original model. We prove that any language accepted by an updatable timed automaton (from classes where emptiness is decidable) is also accepted by a “classical” timed automaton. We propose even more precise results on bisimilarity between updatable and classical timed automata.