Nicolas Markey

Abstract

ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities "Next", "Always" and "Until") has to be completed in order to express the duals of its modalities: it is necessary to add the modality "Release". We then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is Δ2P and Δ3P-complete, depending on the underlying multi-agent model (ATS and CGS, resp.). We also prove that ATL+ model-checking is Δ3P-complete over both models, even with a fixed number of agents.

@inproceedings{fossacs2007-LMO,
  author =              {Laroussinie, Fran{\c c}ois and Markey, Nicolas and
                         Oreiby, Ghassan},
  title =               {On the Expressiveness and Complexity of~{ATL}},
  editor =              {Seidl, Helmut},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'07)},
  acronym =             {{FoSSaCS}'07},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {4423},
  pages =               {243-257},
  year =                {2007},
  month =               mar,
  doi =                 {10.1007/978-3-540-71389-0_18},
  abstract =            {ATL is a temporal logic geared towards the
                         specification and verification of properties in
                         multi-agents systems. It allows to reason on the
                         existence of strategies for coalitions of agents in
                         order to enforce a given property. We prove that the
                         standard definition of~ATL (built on modalities
                         {"}Next{"}, {"}Always{"} and~{"}Until{"}) has to be
                         completed in order to express the duals of its
                         modalities: it~is necessary to add the modality
                         {"}Release{"}. We~then precisely characterize the
                         complexity of ATL model-checking when the number of
                         agents is not fixed. We prove that it is
                         \(\Delta_{2}^{P}\) and \(\Delta_{3}^{P}\)-complete,
                         depending on the underlying multi-agent model (ATS
                         and CGS,~resp.). We also prove that~ATL\({}^{+}\)
                         model-checking is \(\Delta_{3}^{P}\)-complete over
                         both models, even with a fixed number of agents.},
}