Nicolas Markey

Abstract

We propose a new model for timed games, based on concurrent game structures (CGSs). Compared to the classical timed game automata of Asarin et al., 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.

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 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 Henzinger et al.

@inproceedings{concur2007-BLMO,
  author =              {Brihaye, {\relax Th}omas and Laroussinie, Fran{\c
                         c}ois and Markey, Nicolas and Oreiby, Ghassan},
  title =               {Timed Concurrent Game Structures},
  editor =              {Caires, Lu{\'\i}s and Vasconcelos, Vasco T.},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'07)},
  acronym =             {{CONCUR}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4703},
  pages =               {445-459},
  year =                {2007},
  month =               sep,
  doi =                 {10.1007/978-3-540-74407-8_30},
  abstract =            {We propose a new model for timed games, based on
                         concurrent game structures~(CGSs). Compared to the
                         classical \emph{timed game automata} of~Asarin
                         \emph{et~al.}, 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 \emph{et~al.}\par We prove that our model
                         has nice properties, in particular that
                         model-checking timed CGSs against timed
                         \(\textsf{ATL}\) is decidable \emph{via} region
                         abstraction, and in particular that strategies are
                         {"}region-stable{"} if winning objectives are. We
                         also propose a new extension of \(\textsf{TATL}\),
                         containing~\(\textsf{ATL}^{*}\), which we
                         call~\(\textsf{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 Henzinger \emph{et~al.}},
}