Where :

Laboratoire Spécification et Vérification

École Normale Supérieure de Cachan

61, avenue du Président Wilson

94235 Cachan CEDEX

FRANCE

Title : Antichains for parity games

Keywords:

finite automata theory, algorithms, data structures.

Description of the internship :

Parity games are two-players games played on graphs using a token. The players can move the token from the current vertex to an adjacent vertex, in a turn-based fashion. A play is thus a (infinite) sequence of vertices. The so-called parity condition describes the set of winning sequences for each player. The parity condition is very general and it allows to express for instance: reachability conditions (a sequence is winning if it contains an accepting vertex), safety conditions (a sequence is winning if it contains no accpeting vertex), or Büchi conditions (a sequence is winning if it contains an infinite number of occurrence of an accepting vertex). No polynomial-time algorithm is known to solve general parity games.

On the other hand, the technique of antichains has recently been introduced to fight the combinatorial explosion in classical problems of finite automata theory. For instance, promising results have been obtained for the universality problem (which asks whether a given finite automaton accepts every finite word) which has exponential complexity [2]. This technique relies on identifying and exploiting the structure of the underlying graphs. In the case of the universality problem, we use the (determinization) subset construction for finite automata, and this construction has specific properties that can be very useful algorithmically. In practice, this technique can deal with automata of 10,000 states while classical approaches are limited to a few hundred of states.

The ingredients of this success (a problem on finite-state models, with exponential complexity, and with particular structure) call for applying the antichain technique to parity games.

During this internship, we will focus on an algorithmic solution using antichains for solving parity games. We will start from a translation of parity games to safety games, and on the existence of functions called small progress measures which, when they satisfy local conditions on a graph, guarantee non-local conditions such as the existence of a winning strategy for one of the players [1, 3]. These functions give a structure to parity games that can be exploited to define an antichain algorithm. The intern shall define and implement this new algorithm, study or propose suited data structures, and compare (theoretically and practically) this new algorithm with the state-of-the-art solutions.

Contact :

Laurent Doyen

Tél: +33 (0)1 47 40 77 06

Email: doyen@lsv.ens-cachan.fr

References

[1]: J. Bernet, D. Janin, and I. Walukiewicz. Permissive strategies: from parity games to safety games. Inf. Théorique et Applications, 36(3):261–275, 2002.
[2]: M. De Wulf, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Antichains: A new algorithm for checking universality of finite automata. In Proceedings of CAV 2006: Computer-Aided Verification, Lecture Notes in Computer Science 4144, pages 17–30. Springer-Verlag, 2006.
[3]: M. Jurdzinski. Small progress measures for solving parity games. In Proc. of STACS: Theor. Aspects of Comp. Sc., LNCS 1770, pages 290–301. Springer, 2000.

Laboratoire Spécification et Vérification

This document was translated from L^AT_EX by H^EV^EA.