Search

• < Previous
• 1
• Next >

---

Model Checking One-clock Priced Timed Automata

Patricia Bouyer ; Kim G. Larsen ; Nicolas Markey.

We consider the model of priced (a.k.a. weighted) timed automata, an extension of timed automata with cost information on both locations and transitions, and we study various model-checking problems for that model based on extensions of classical temporal logics with cost constraints on modalities.&nbsp;[&hellip;]

---

Stochastic Timed Automata

Nathalie Bertrand ; Patricia Bouyer ; Thomas Brihaye ; Quentin Menet ; Christel Baier ; Marcus Groesser ; Marcin Jurdzinski.

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&nbsp;[&hellip;]

---

Pure Nash Equilibria in Concurrent Deterministic Games

Patricia Bouyer ; Romain Brenguier ; Nicolas Markey ; Michael Ummels.

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&nbsp;[&hellip;]

---

Reconfiguration and Message Losses in Parameterized Broadcast Networks

Nathalie Bertrand ; Patricia Bouyer ; Anirban Majumdar.

Broadcast networks allow one to model networks of identical nodes communicating through message broadcasts. Their parameterized verification aims at proving a property holds for any number of nodes, under any communication topology, and on all possible executions. We focus on the coverability&nbsp;[&hellip;]

---

Games Where You Can Play Optimally with Arena-Independent Finite Memory

Patricia Bouyer ; Stéphane Le Roux ; Youssouf Oualhadj ; Mickael Randour ; Pierre Vandenhove.

For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in&nbsp;[&hellip;]

---

Half-Positional Objectives Recognized by Deterministic B\"uchi Automata

Patricia Bouyer ; Antonio Casares ; Mickael Randour ; Pierre Vandenhove.

In two-player games on graphs, the simplest possible strategies are those that can be implemented without any memory. These are called positional strategies. In this paper, we characterize objectives recognizable by deterministic B\"uchi automata (a subclass of omega-regular objectives) that are&nbsp;[&hellip;]

---