Timed Concurrent Game Structures

Thomas Brihaye
LSV, Cachan
Friday, 7 December, 2007 (All day)

We propose a new model for timed games, based on concurrent game structures. At each step of such a game, each player chooses a delay and a move function. The smallest chosen delay then elapses, and a transition is fired according to the values of all the move functions at that time.

Compared to the classical timed game automata of Asarin et al. [AMPS98], our timed~CGSs are ``more concurrent'', in the sense that they always allow all the agents to act on the system, independently of the delay they want to elapse before their action. Timed CGSs weaken the ``element of surprise'' of timed game automata reported by de Alfaro et al. [AFHM+03].

We prove that our model has nice properties, in particular that model-checking timed CGSs against timed ATL is decidable via region abstraction, and in particular that strategies (and move functions) are ``region-stable'' if winning objectives are. We also propose a new extension of TATL, containing ATL*, which we call TALTL. We prove that model-checking this logic remains decidable on timed CGSs. Last, we explain how our algorithms can be adapted in order to rule out Zeno (co-)strategies, based on the ideas of de Alfaro et al. [AFHM+03,HP06].

Joint work with François Laroussinie, Nicolas Markey and Ghassan Oreiby