# Patricia Bouyer - LSV & ENS Cachan

## Contact Details

NamePatricia Bouyer |
||

AffiliationLSV & ENS Cachan |
||

CityCachan |
||

CountryFrance |
||

## Pubs By Year |
||

## External Links |
||

## Pub CategoriesComputer Science - Logic in Computer Science (13) Computer Science - Computer Science and Game Theory (10) Computer Science - Computational Complexity (4) Mathematics - Information Theory (1) Computer Science - Information Theory (1) |

## Publications Authored By Patricia Bouyer

A decade ago, Abdulla et al introduced the elegant concept of decisiveness for denumerable Markov chains [1]. Roughly decisiveness allows one to lift most good properties from finite Markov chains to denumerable ones, and therefore to adapt existing verification algorithms to infinite-state models. Denumerable Markov chains however do not encompass stochastic real-time systems, and general stochastic transition systems (STSs) are needed. Read More

We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. While several results have been obtained on these games recently, decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) remained open; in particular, so far there was no known upper bound on the memory that is required for winning strategies. By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the density of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. Read More

Dynamic complexity is concerned with updating the output of a problem when the input is slightly changed. We study the dynamic complexity of Dyck reachability problems in directed and undirected graphs, where updates may add or delete edges. We show a strong dichotomy between such problems, based on the size of the Dyck alphabet. Read More

Dynamic complexity is concerned with updating the output of a problem when the input is slightly changed. We study the dynamic complexity of two-player parity games over graphs of bounded tree-width, where updates may add or delete edges, or change the owner or color of states. We show that this problem is in DynFO (with LOGSPACE precomputation); this is achieved by a reduction to a Dyck-path problem on an acyclic automaton. Read More

**Affiliations:**

^{1}LSV, CNRS and ENS Cachan, Université Paris-Saclay, France,

^{2}LSV, CNRS and ENS Cachan, Université Paris-Saclay, France,

^{3}LSV, CNRS and ENS Cachan, Université Paris-Saclay, France

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. Read More

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\frac{1}{2}$-player, $1\frac{1}{2}$-player, and $\frac{1}{2}$-player games where the $\frac{1}{2}$ symbolizes the presence of the stochastic "nature" player. For STGs with reachability objectives it is known that $1\frac{1}{2}$-player one-clock STGs are decidable for qualitative objectives, and that $2\frac{1}{2}$-player three-clock STGs are undecidable for quantitative reachability objectives. Read More

We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Read More

Weighted timed automata have been defined in the early 2000's for modelling resource-consumption or -allocation problems in real-time systems. Optimal reachability is decidable in weighted timed automata, and a symbolic forward algorithm has been developed to solve that problem. This algorithm uses so-called priced zones, an extension of standard zones with cost functions. Read More

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. Read More

**Authors:**Patricia Bouyer

^{1}, Nicolas Markey

^{2}, Mickael Randour

^{3}, Kim G. Larsen

^{4}, Simon Laursen

^{5}

**Affiliations:**

^{1}LSV - CNRS and ENS Cachan - France,

^{2}LSV - CNRS and ENS Cachan - France,

^{3}LSV - CNRS and ENS Cachan - France,

^{4}Aalborg University - Denmark,

^{5}Aalborg University - Denmark

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. Read More

**Affiliations:**

^{1}LSV -- ENS Cachan & CNRS,

^{2}LSV -- ENS Cachan & CNRS,

^{3}LSV -- ENS Cachan & CNRS,

^{4}TU Dresden

We study pure-strategy Nash equilibria in multi-player concurrent deterministic games, for a variety of preference relations. We provide a novel construction, called the suspect game, which transforms a multi-player concurrent game into a two-player turn-based game which turns Nash equilibria into winning strategies (for some objective that depends on the preference relations of the players in the original game). We use that transformation to design algorithms for computing Nash equilibria in finite games, which in most cases have optimal worst-case complexity, for large classes of preference relations. Read More

**Authors:**Nathalie Bertrand

^{1}, Patricia Bouyer

^{2}, Thomas Brihaye

^{3}, Quentin Menet

^{4}, Christel Baier

^{5}, Marcus Groesser

^{6}, Marcin Jurdzinski

^{7}

**Affiliations:**

^{1}INRIA Rennes - Bretagne Atlantique,

^{2}LSV & ENS Cachan,

^{3}Université de Mons,

^{4}Université de Mons,

^{5}Technische Universität Dresden,

^{6}Technische Universität Dresden,

^{7}University of Warwick

A stochastic timed automaton is a purely stochastic process defined on a timed automaton, in which both delays and discrete choices are made randomly. We study the almost-sure model-checking problem for this model, that is, given a stochastic timed automaton A and a property $\Phi$, we want to decide whether A satisfies $\Phi$ with probability 1. In this paper, we identify several classes of automata and of properties for which this can be decided. Read More

**Affiliations:**

^{1}LSV -- CNRS & ENS Cachan,

^{2}LSV -- CNRS & ENS Cachan,

^{3}DTU, Kgs. Lyngby

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. Read More

The languages of infinite timed words accepted by timed automata are traditionally defined using Buchi-like conditions. These acceptance conditions focus on the set of locations visited infinitely often along a run, but completely ignore quantitative timing aspects. In this paper we propose a natural quantitative semantics for timed automata based on the so-called frequency, which measures the proportion of time spent in the accepting locations. Read More

We study nondeterministic strategies in parity games with the aim of computing a most permissive winning strategy. Following earlier work, we measure permissiveness in terms of the average number/weight of transitions blocked by the strategy. Using a translation into mean-payoff parity games, we prove that the problem of computing (the permissiveness of) a most permissive winning strategy is in NP intersected coNP. Read More

In this paper, we consider reachability games over general hybrid systems, and distinguish between two possible observation frameworks for those games: either the precise dynamics of the system is seen by the players (this is the perfect observation framework), or only the starting point and the delays are known by the players (this is the partial observation framework). In the first more classical framework, we show that time-abstract bisimulation is not adequate for solving this problem, although it is sufficient in the case of timed automata . That is why we consider an other equivalence, namely the suffix equivalence based on the encoding of trajectories through words. Read More

We consider the model of priced (a.k.a. Read More

**Authors:**Patricia Bouyer

^{1}, Nicolas Markey

^{2}, Joël Ouaknine

^{3}, Philippe Schnoebelen

^{4}, James Worrell

**Affiliations:**

^{1}LSV,

^{2}LSV,

^{3}LSV,

^{4}LSV

A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with insertion errors, i.e. Read More