Quantitative Strategic Reasoning

Presentation

Strategic reasoning is a powerful approach to the verification and synthesis of reliable computer systems, for which several logics have recently been defined. Our aim in this project is to further develop this line of research by incorporating quantitative aspects, e.g. modelling timing aspects, energy consumption or stochastic behaviours. A long-term goal is to develop notions of quality of strategies, with the aim of optimising these measures.

Research programme

Our workplan can be presented along three axes:
Task 1: measuring the quality of strategies
In fuzzy logics, state predicates are not Boolean but take values in the interval [0,1]. This extension may be used to model precision or vagueness, and has been successfully used in various industrial applications. Its adaptation to strategic reasoning provides a way of measuring the quality of strategies. We recently obtained positive results in that direction, which raised several new questions, such as stability (how the values of formulas may change when the values of atomic propositions change), identification of fragments with more efficient model-checking algorithms, or extension to fuzzy strategies.
Task 2: measuring the efficiency of strategies
Optimizing quantities over plays (e.g. energy consumption) is a must-have in many applications. Recent results showed that combining such quantitative constraints on top of Strategy Logic renders verification undecidable, but exhibited nice periodicity properties for fragments of the logic. We will explore this direction further, and consider other quantitative constraints (such as mean payoff)
Task 3: measuring the needed knowledge of strategies.
Strategies are based on what players observe. In many situations, they cannot observe the whole system, which may dramatically reduce the quality or efficiency of the strategy. In Task 3, we aim e.g. at allowing players to buy and use additional sensors, so as to have better knowledge of the evolution of the system and apply more specific strategies. This extends various works within a quantitative logical framework.

Partners

QuaSL is an associate team involving

Publications

Joint publications by QuaSL teams

[BKM+23] Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano, and Giuseppe Perelli. Reasoning about Quality and Fuzziness of Strategic Behaviours. ACM Transactions on Computational Logic. ACM Press, 2023. To appear. 
@article{tocl2023-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},
  year =                {2023},
  note =                {To~appear},
}
[BFF+21] Raphaël Berthon, Nathanaël Fijalkow, Emmanuel Filiot, Shibashis Guha, Bastien Maubert, Aniello Murano, Laureline Pinault, Sophie Pinchinat, Sasha Rubin et Olivier Serre. Alternating Tree Automata with Qualitative Semantics. ACM Transactions on Computational Logic 22(1):7:1-7:24. ACM Press, January 2021. 
@article{tocl22(1)-BFFGMMPPRS,
  author =              {Berthon, Rapha{\"e}l and Fijalkow, Nathana{\"e}l and
                         Filiot, Emmanuel and Guha, Shibashis and Maubert,
                         Bastien and Murano, Aniello and Pinault, Laureline
                         and Pinchinat, Sophie and Rubin, Sasha and Serre,
                         Olivier},
  title =               {Alternating Tree Automata with Qualitative
                         Semantics},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {22},
  number =              {1},
  pages =               {7:1-7:24},
  year =                {2021},
  month =               jan,
  doi =                 {10.1145/3431860},
}
[MPS+21] Bastien Maubert, Sophie Pinchinat, François Schwarzentruber et Silvia Stranieri. Concurrent Games in Dynamic Epistemic Logic. In IJCAI'20, pages 1877-1883. IJCAI organization, January 2021. 
@inproceedings{ijcai2020-MPSS,
  author =              {Maubert, Bastien and Pinchinat, Sophie and
                         Schwarzentruber, Fran{\c c}ois and Stranieri,
                         Silvia},
  title =               {Concurrent Games in Dynamic Epistemic Logic},
  editor =              {Bessiere, Christian},
  booktitle =           {{P}roceedings of the 29th {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'20)},
  acronym =             {{IJCAI}'20},
  publisher =           {IJCAI organization},
  pages =               {1877-1883},
  year =                {2021},
  month =               jan,
  doi =                 {10.24963/ijcai.2020/260},
}

Publications before QuaSL

[MMP+20] Bastien Maubert, Aniello Murano, Sophie Pinchinat, François Schwarzentruber and Silvia Stranieri. Dynamic Epistemic Logic Games with Epistemic Temporal Goals. Technical Report 2001-07141, arXiv, January 2020. 
@techreport{arxiv2001.07141-MMSSS,
  author =              {Maubert, Bastien and Murano, Aniello and Pinchinat,
                         Sophie and Schwarzentruber, Fran{\c c}ois and
                         Stranieri, Silvia},
  title =               {Dynamic Epistemic Logic Games with Epistemic
                         Temporal Goals},
  number =              {2001-07141},
  year =                {2020},
  month =               jan,
  institution =         {arXiv},
}
[BKM+19] Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano et Giuseppe Perelli. Reasoning about Quality and Fuzziness of Strategic Behaviours. In IJCAI'19, pages 1588-1594. IJCAI organization, août 2019. 
@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},
}
[KMS19] Sophia Knight, Bastien Maubert and François Schwarzentruber. Reasoning about knowledge and messages in asynchronous multi-agent systems. Mathematical Structures in Computer Science 29(1):127-168. January 2019. 
@article{mscs29(1)-KMS,
  author =              {Knight, Sophia and Maubert, Bastien and
                         Schwarzentruber, Fran{\c c}ois},
  title =               {Reasoning about knowledge and messages in
                         asynchronous multi-agent systems},
  journal =             {Mathematical Structures in Computer Science},
  volume =              {29},
  number =              {1},
  pages =               {127-168},
  year =                {2019},
  month =               jan,
  doi =                 {10.1017/S0960129517000214},
}
[MPS19] Bastien Maubert, Sophie Pinchinat and François Schwarzentruber. Reachability Games in Dynamic Epistemic Logic. In IJCAI'19, pages 499-505. IJCAI organization, August 2019. 
@inproceedings{ijcai2019-MSS,
  author =              {Maubert, Bastien and Pinchinat, Sophie and
                         Schwarzentruber, Fran{\c c}ois},
  title =               {Reachability Games in Dynamic Epistemic Logic},
  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 =               {499-505},
  year =                {2019},
  month =               aug,
  doi =                 {10.24963/ijcai.2019/71},
}
[DMP18] Cătălin Dima, Bastien Maubert and Sophie Pinchinat. Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus. ACM Transactions on Computational Logic 19(3):23:1-23:33. ACM Press, September 2018. 
@article{tocl19(3)-DMS,
  author =              {Dima, C{\u a}t{\u a}lin and Maubert, Bastien and
                         Pinchinat, Sophie},
  title =               {Relating Paths in Transition Systems: The~Fall of
                         the Modal Mu-Calculus},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {19},
  number =              {3},
  pages =               {23:1-23:33},
  year =                {2018},
  month =               sep,
  doi =                 {10.1145/3231596},
}