The element of surprise in timed games

In synthesis and control, it is natural to view a system and its
environment as players of a game that pursue different objectives;
in modular verification it is often appropriate to model the system
components as (competing or cooperating) players.

In this talk, I will consider concurrent two-person timed games,
in which the players decide have to not only decide which action
to play, but also when to play it.

Such timed games differ from untimed games in two essential ways.
First, players can take each other by surprise, because actions are
played with delays that cannot be anticipated by the opponent.
Second, a player should not be able to win the game by preventing time
from diverging.

We present a model of timed games that preserves the element of surprise
and accounts for time divergence in a way that treats both players
completely symmetrically and applies to all omega-regular winning
conditions.
I will show that:
- Timed games are not determined, i.e. there are games in which
no player wins.

- The ability to take each other by surprise adds extra power to the
players.

- Memory strategies are more powerful than memoryless strategies
already in the case of reachability objectives.

- The set of states from which a given player can win an omega-regular
objective can be computed symbolically for games specified
in the style of timed automata.

(joint work with Luca de Alfaro, Marco Faella, Thomas A. Henzinger,
Rupak Majumdar.)