Nicolas Markey

Résumé

We introduce and study SL[F]—a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an SL[F] formula is a real value in [0,1], reflecting "how much" or "how well" the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of SL[F] in quantitative reasoning about multi-agent systems, by showing how it can express concepts of stability in multi-agent systems, and how it generalises some fuzzy temporal logics. We also provide a model-checking algorithm for our logic, based on a quantitative extension of Quantified CTL.

@inproceedings{ijcai2019-BKMMMP,
  author =              {Bouyer, Patricia and Kupferman, Orna and Markey,
                         Nicolas and Maubert, Bastien and Murano, Aniello and
                         Perelli, Giuseppe},
  title =               {Reasoning about Quality and Fuzziness of Strategic
                         Behaviours},
  editor =              {Kraus, Sarit},
  booktitle =           {{P}roceedings of the 28th {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'19)},
  acronym =             {{IJCAI}'19},
  publisher =           {IJCAI organization},
  pages =               {1588-1594},
  year =                {2019},
  month =               aug,
  doi =                 {10.24963/ijcai.2019/220},
  abstract =            {We~introduce and study
                         {\(\textsf{SL}[\mathcal{F}]\)}---a~quantitative
                         extension of {\(\textsf{SL}\)} (Strategy Logic),
                         one~of the most natural and expressive logics
                         describing strategic behaviours. The satisfaction
                         value of an {\(\textsf{SL}[\mathcal{F}]\)} formula
                         is a real value in~{\([0,1]\)}, reflecting {"}how
                         much{"} or {"}how well{"} the strategic on-going
                         objectives of the underlying agents are satisfied.
                         We~demonstrate the applications of
                         {\(\textsf{SL}[\mathcal{F}]\)} in quantitative
                         reasoning about multi-agent systems, by showing how
                         it can express concepts of stability in multi-agent
                         systems, and how it generalises some fuzzy temporal
                         logics. We~also provide a model-checking algorithm
                         for our logic, based on a quantitative extension of
                         Quantified~\textsf{CTL}.},
}