Nicolas Markey

Résumé

Temporal logics are extensively used for the specification of on-going behaviors of computer systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviors in multi-agent systems, and the transition of temporal logics to a quantitative setting, where different satisfaction values enable the specifier to formalize concepts such as certainty or quality. In the first class, SL (Strategy Logic) is one of the most natural and expressive logics describing strategic behaviors. In the second class, a notable logic is LTL[F], which extends LTL with quality operators.

In this work we introduce and study SL[F], which enables the specification of quantitative strategic behaviors. 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, showing how it can express and measure concepts like stability in multi-agent systems, and how it generalizes some fuzzy temporal logics. We also provide a model-checking algorithm for SL[F], based on a quantitative extension of Quantified CTL*. Our algorithm provides the first decidability result for a quantitative extension of Strategy Logic. In addition, it can be used for synthesizing strategies that maximize the quality of the systems' behavior

@article{tocl24(3)-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},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {24},
  number =              {3},
  pages =               {21:1-21:38},
  year =                {2023},
  month =               jul,
  doi =                 {10.1145/3582498},
  abstract =            {Temporal logics are extensively used for the
                         specification of on-going behaviors of computer
                         systems. Two significant developments in this area
                         are the extension of traditional temporal logics
                         with modalities that enable the specification of
                         on-going strategic behaviors in multi-agent systems,
                         and the transition of temporal logics to a
                         quantitative setting, where different satisfaction
                         values enable the specifier to formalize concepts
                         such as certainty or quality. In~the first class,
                         SL~(Strategy~Logic)~is one of the most natural and
                         expressive logics describing strategic behaviors. In
                         the second class, a notable logic is
                         \(\textsf{LTL}[\mathcal{F}]\), which extends
                         \textsf{LTL} with quality operators. \par In~this
                         work we introduce and study
                         \(\textsf{SL}[\mathcal{F}]\), which enables the
                         specification of quantitative strategic behaviors.
                         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,
                         showing how it can express and measure concepts like
                         stability in multi-agent systems, and how it
                         generalizes some fuzzy temporal logics. We also
                         provide a model-checking algorithm for
                         \(\textsf{SL}[\mathcal{F}]\), based on a
                         quantitative extension of
                         Quantified~\(\textsf{CTL}^*\). Our~algorithm
                         provides the first decidability result for a
                         quantitative extension of Strategy Logic. In
                         addition, it can be used for synthesizing strategies
                         that maximize the quality of the systems' behavior},
}