Workshop on Games for Design, Verification and Synthesis |
Colocated with CAV'09 Grenoble (France), 28 June 2009 |
Scope of the workshop
GASICS is an ESF project of the EUROCORES programme LogICCC (Modelling intelligent interaction – Logic in the Humanities, Social and Computational sciences ). It studies game theoretic formalizations of interactive computational systems and algorithms for their analysis and synthesis. Our aim is to extend the existing notions of games played on graphs introduced by computer scientists. Currently, most of the games played on graphs are of the sort "two-player zero-sum", we aim to extend them to "multiple-player non-zero-sum", and show the applicability of the new theory to the analysis and synthesis of interactive computational systems.
The aim of this workshop is to bring together researchers working on game-related subjects, and to discuss on various aspects of game theory in the fields where it is applied. The workshop will be composed of two invited talks, together with contributed talks on the following (non-exhaustive) list of relevant topics:
- Adapted notions of games for synthesis of complex interactive computational systems
- Games played on complex and infinite graphs
- Games with quantitative objectives
- Game with incomplete information and over dynamic structures
- Heuristics for efficient game solving.
Invited speakers
- Luca De Alfaro:
Stochastic Reachability and Safety Games
We consider repeated games over finite state spaces played for an infinite number of rounds; at each round, the two players choose simultaneously and independently a move, and the two moves jointly determine the successor state. Such games can be used to solve problems in fields as different as optimal control and verification. Among the simplest objectives, for a player, are reachabilty and safety. The reachability objective consists in reaching a set of target states; the safety objective consists in confining the set of visited states within a given safe set. The value of a reachability or safety game is the maximal probability with which a player can ensure that the objective is attained.
The traditional approach to solving reachability and safety games is based on a value-iteration approach, which computes a sequence of values converging to the value of the game. This approach, however, presents three drawbacks: (a) even though memoryless strategies suffice for reachability, the value-iteration approach allows only for the determination of memory-dependent strategies; (b) no winning strategies for safety games can be obtained, and (c) value-iteration only yields lower (resp. upper) bounds for the value of reachability(resp. safety) games (without matching upper, resp. lower, bounds). We show that all three problems can be solved via approaches based on strategy, rather than value, iteration, and we present convergent strategy iteration schemes for reachability and safety games. Such strategy iteration schemes provide memoryless strategies that achieve the value of the games within any desired accuracy, and as a consequence, also converging upper and lower bounds for the value of reachability and safety games.
- Peter Bro Miltersen:
Some recent results and some open problems concerning solving infinite duration games.
We describe a number of recent algorithmic results on solving two-player, zero-sum, infinite duration games played on finite graphs. Each result is accompanied by an open problem.
The talk will touch upon joint work with Daniel Andersson, Kristoffer Arnsfelt Hansen, Thomas Dueholm Hansen, Vladimir Gurvich, Michal Koucky, and Troels Bjerre Sĝrensen.
Programme
08:55 - 09:00 | Welcome — Introduction |
09:00 - 10:00 |
Luca De Alfaro (invited talk)
Stochastic Reachability and Safety Games
|
10:00 - 10:30 | Coffee break |
10:30 - 11:00 | Wladimir Fridman and Jörg Olschewski |
11:00 - 11:30 | Michael Ummels and Dominik Wojtczak |
11:30 - 12:00 |
Arnaud Da Costa
|
12:00 - 14:00 | Lunch |
14:00 - 15:00 | Peter Bro Miltersen (invited talk) |
15:00 - 15:30 | John Fearnley, Marcin Jurdziński, and Rahul Savani |
15:30 - 16:00 | Coffee break |
16:00 - 16:30 | Laurent Doyen, Gilles Geeraerts, Jean-François Raskin, and Julien Reichert |
16:30 - 17:00 | Alexandre David, Kim G. Larsen, and Didier Lime |
17:00 - 17:30 | Roderick Bloem, Karin Greimel, Thomas A. Henzinger, and Barbara Jobstmann |
17:30 - 18:00 | Robert Könighofer, Georg Hofferek, and Roderick Bloem |
18:00 - 18:01 | Closing |
Organizers
Programme Committee
- Véronique Bruyère
- Marcin Jurdziński
- Kim G. Larsen
- Nicolas Markey
- Jean-François Raskin
- Pierre-Yves Schobbens
- Olivier Serre
- Wolfgang Thomas
Page maintained by Nicolas Markey.
Last modified: 23 July 2009.