Nicolas Markey

Abstract

We extend the framework of ATL model-checking to "simply timed" concurrent game structures, i.e., multi-agent structures where each transition carry an integral duration (or interval thereof). While the case of single durations is easily handled from the semantics point of view, intervals of durations raise several interesting questions. Moreover subtle algorithmic problems have to be handled when dealing with model checking. We propose a semantics for which we develop efficient (PTIME) algorithms for timed ATL without equality constraints, while the general case is shown to be EXPTIME-complete.

@inproceedings{formats2006-LMO,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Oreiby, Ghassan},
  title =               {Model-Checking Timed~{ATL} for Durational Concurrent
                         Game Structures},
  editor =              {Asarin, Eugene and Bouyer, Patricia},
  booktitle =           {{P}roceedings of the 4th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'06)},
  acronym =             {{FORMATS}'06},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4202},
  pages =               {245-259},
  year =                {2006},
  month =               sep,
  doi =                 {10.1007/11867340_18},
  abstract =            {We extend the framework of ATL model-checking to
                         {"}simply timed{"} concurrent game structures, i.e.,
                         multi-agent structures where each transition carry
                         an integral duration (or interval thereof). While
                         the case of single durations is easily handled from
                         the semantics point of view, intervals of durations
                         raise several interesting questions. Moreover subtle
                         algorithmic problems have to be handled when dealing
                         with model checking. We propose a semantics for
                         which we develop efficient (PTIME) algorithms for
                         timed ATL without equality constraints, while the
                         general case is shown to be EXPTIME-complete.},
}