My (recent) slides feature a clockwork on the top-right corner;
this is a non-original creation by the Internet (forgot who...), Victor Marsault and myself.
Find out more about it here.
Boundedness games (based on joint works with Krishnendu Chatterjee, Thomas Colcombet, Florian Horn and Martin Zimmermann)
In this talk, I will discuss some recent developments about boundedness games, which appear in different contexts, for instance in the study of regular cost-functions as defined by Thomas Colcombet.
They are two-player games featuring counters that can be incremented, reset of left unchanged, and where the first player's objective is that the counters remain bounded along the play. They can be played over finite graphs or infinite graphs, for instance over pushdown graphs. I am interested in the following questions: deciding the winner, proving the existence of finite-memory strategies, and constructing such strategies.
- Presentation for the Séminaire de l'Equipe MoVe du Laboratoire d'Informatique Fondamentale, Marseille, France (02/05/2013)
[PDF]
- Presentation for the Séminaire Algorithmique du Laboratoire d'informatique Gaspard-Monge, Marne-la-Vallée, France (16/04/2013)
[PDF]
Emptiness of alternating tree automata through games of imperfect information (joint work with Sophie Pinchinat and Olivier Serre)
In this talk, I will consider the emptiness problem for alternating tree automata with two different acceptance semantics: classical (all branches are accepted) and qualitative (almost all branches are accepted).
I will show a new approach to tackle these problems, through games of imperfect information, and argue that this technique provides new answers as well as new questions: first, it shows the decidability of the emptiness problem for alternating (Buechi) tree automata with qualitative semantics, and second, it is generic in the sense that it only relies on a positionality result and decidability of the corresponding imperfect information games.
- Presentation for Seminarium Teoria Automatów, Warsaw, Poland (20/03/2013)
Cost-parity games and Cost-Streett games (Gry parzystosci z licznikami) (joint work with Martin Zimmermann)
The starting point of this work is the following observation: although similar in flavor, parity games and finitary parity games are very different from an algorithmic perspective. Both are two-player games on graphs whose vertices are labeled by integers. The parity winning condition states that almost all odd labels are followed by a greater even label. Parity games have received a lot of attention since they are the model-checking games of the modal mu-calculus and determining the winner in a parity game is one of the few problems in NP and co-NP, but not known to be in PTIME. The finitary parity condition is obtained by additionally requiring a bound on the number of edges traversed between odd labels and the next greater even label. Quite surprisingly, deciding the winner in a finitary parity game can be carried out in polynomial time.
This work generalizes both parity games and finitary parity games by introducing cost-parity games. In these games traversing an edge comes with a cost and the condition requires a bound on the cost between odd labels and the next greater even label. We show that cost-parity games enjoy two nice properties of parity and finitary parity games: the first player has memoryless winning strategies, and determining the winner lies in NP and co-NP (as for parity games). Furthermore, we show that solving cost-parity games can be algorithmically reduced to solving parity games, which allows to solve cost-parity games almost as efficiently as parity games.
- Presentation for FSTTCS'2012, Hyderabad, India (15/12/2012) [PDF]
- Presentation for the annual meeting of Groupe de Travail Jeux, Cachan, France (21/09/2012) [PDF]
- Presentation for GAMES'2012, Naples, Italy (11/09/2012) [PDF]
- Presentation for Seminarium Teoria Automatów, Warsaw, Poland (20/06/2012)
Deciding the value 1 problem for probabilistic leaktight automata (joint work with Hugo Gimbert and Youssouf Oualhajd)
In this talk, I will present some recent work on the value 1 problem for probabilistic automata over finite words: given a probabilistic automaton, are there words accepted with probability arbitrarily close to 1?
This problem was proved undecidable recently. However, it shows some similarities with another problem, the boundedness problem for distance automata, which was shown decidable by Hashiguchi in 1982. Initially derived from a very long and complicated proof, this decidability result has been considerably simplified, the major steps being an algebraic algorithm proposed by Leung in 1991 and algebraic techniques developed by Simon in 1990 and 1994. The decidability result was later extended to nested desert distance automata and conceptually simplified by Kirsten in 2005.
We have transferred the underlying ideas to probabilistic automata. Our main contribution is to introduce a new class of probabilistic automata, called leaktight automata, for which the value 1 problem is shown decidable (and PSPACE-complete). We construct an algorithm based on the computation of a monoid abstracting the behaviors of the automaton, following Leung's algorithm. As in the case of distance automata, the correctness proof relies on the algebraic techniques developed by Simon, namely factorization and decomposition trees.
- Presentation for the 68NQRT Seminar, Rennes, France (24/01/2013) [PDF]
- Presentation for the conference LICS (Logics in Computer Science), Dubrovnik, Croatia (26/06/2012) [PDF]
- Presentation for WATA'2012, Dresden, Germany (31/05/2012) [PDF] (Please pay attention to the top-right clock, a non-original creation by Victor Marsault and myself)
- Presentation for Seminarium Teoria Automatów, Warsaw, Poland (09/05/2012)
- Presentation for Séminaire de l'équipe Automates et Applications, Paris, France (25/11/2011) [PDF]
How much memory is needed to win regular games? (joint work with Thomas Colcombet and Florian Horn)
Games on graphs provide a natural model for reactive systems.
In this talk, we consider games with an external winning condition
given by a regular language over finite words.
The first player, Eve, tries to ensure that a finite prefix of the play
belongs to the language, while the second player, Adam,
tries to spoil this objective.
Given an external condition described by a regular language,
we study the memory required to construct optimal strategies in any arena.
- Presentation for GAMES'2011, Paris, France (01/09/2011) [PDF]
Reducing parity games to simple stochastic games (joint work with Krishnendu Chatterjee and Florian Horn)
Games on graphs provide a natural model for reactive non-terminating systems. In such games, the interaction of two players on an arena results in an infinite path that describes a run of the system. Different settings are used to model various open systems in computer science, as for instance turn-based or concurrent moves, and deterministic or stochastic transitions. In this paper, we are interested in turn-based games, and specifically in deterministic parity games and stochastic reachability games (also known as simple stochastic games). We present a simple, direct and efficient reduction from deterministic parity games to simple stochastic games: it yields an arena whose size is linear up to a logarithmic factor in size of the original arena.
- Presentation for GanDALF'2011, Minori, Italy (15/06/2011) [TAR] (flash presentation using Prezi)
Finitary Languages (joint work with Krishnendu Chatterjee)
The class of omega-regular languages provides a robust specification language in verification. Every omega-regular condition can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens "eventually". Finitary liveness was proposed by Alur and Henzinger as a stronger formulation of liveness. It requires that there exists an unknown, fixed bound b such that something good happens within b transitions. In this work we consider automata with finitary acceptance conditions defined by finitary Buchi, parity and Streett languages. We study languages expressible by such automata: we give their topological complexity and present a regular-expression characterization. We compare the expressive power of finitary automata and give optimal algorithms for classical decisions questions. We show that the finitary languages are Sigma 2-complete; we present a complete picture of the expressive power of various classes of automata with finitary and infinitary acceptance conditions; we show that the languages defined by finitary parity automata exactly characterize the star-free fragment of omega B-regular languages; and we show that emptiness is NLOGSPACE-complete and universality as well as language inclusion are PSPACE-complete for finitary parity and Streett automata.
- Presentation for LATA'2011, Tarragona, Spain (30/05/2011) [PDF]
- Presentation for YR'2010 (Young Researchers), affiliated workshop of CONCUR'2010, Paris,
France (04/09/2010) [PDF]
Exercises in reachability style (joint work with Florian Horn)
Games on graphs provide a natural and powerful model for reactive systems. In this paper, we consider generalized reachability objectives, defined as conjunctions of reachability objectives. We first prove that deciding the winner in such games is PSPACE-complete, although it is fixed-parameter tractable with the number of reachability objectives as parameter. Moreover, we consider the memory requirements for both players and give matching upper and lower bounds on the size of winning strategies. In order to allow more efficient algorithms, we consider subclasses of generalized reachability games. We show that bounding the size of the reachability sets gives two natural subclasses where deciding the winner can be done efficiently.
- Presentation for GASICS' 4th meeting, Paris, France (19/11/2010) [PDF]
- Presentation for GAMES'2010, Oxford, Great-Britain (20/09/2010) [PDF]
Games on graphs
- Presentation for Séminaire Thésards, Paris, France (10/11/2010) [PDF]
