Model Checking of Strategic Timed Temporal Logics (Extended Abstract)

Abstract

Autonomous agents provide a powerful paradigm for modelling and analysing socio-technical systems. They encompass networks of communicating agents that make autonomous decisions based on AI methods. Modeling strategic behaviors in a real-time context is crucial for ensuring the safety and security of agent systems. Alternating-time temporal logic (ATL* ) and its fragment ATL [1, 2] are logics that enable reasoning about strategic interactions in such systems by extending the framework of temporal logic with the game-theoretic concept of strategic ability. Therefore, ATL allows us to express statements about what groups of agents can achieve. These properties are useful for specifying, verifying, and reasoning about interactions in agent systems [11, 12, 7], as well as security and usability in e-voting protocols [5, 9]. They have become particularly relevant due to very active development of algorithms and tools for verification [15, 6, 8, 10], where the “correctness” is defined in terms of strategic ability. In this lecture we investigate timed extensions of strategic logics including ATL and ATL* . We begin with discussing the syntax and semantics of ATL and its discrete time extension TATL [14, 13]. Then, we introduce two new strategy logics: Strategic CTL (SCTL) and its timed extension Strategic Timed CTL (STCTL) [4]. Each (timed) strategy logic is interpreted over two types of structures: models of synchronous (Time) Multi-Agent Systems MAS and of asynchronous (Time) Multi-Agent Systems AMAS. We consider two semantics related to information: imperfect (i) and perfect (I), and two semantics related to recall: imperfect (r) and perfect (R). Additionally, Time MAS and Time AMAS can be either discrete (D) or continuous (C). The lecture focuses on the model checking problem for SCTL and STCTL, considering all the semantics mentioned above, and comparing their complexity with other strategy logics. Notably, we demonstrate that SCTL is more expressive than ATL for all semantics, including

1. Multi-agent Systems and ATL

2. Timed extensions of ATL and SCTL

the timed versions as well. Furthermore, we analyze the model checking problem for diferent combinations of semantics. For instance, the model checking problem for SCTLir has the same complexity as for ATLir, and the model checking problem for STCTLir has the same complexity as for TCTL. Additionally, we provide a practical demonstration of the feasibility of STCTLir model checking using IMITATOR [3].

Acknowledgements This work was funded by the CNRS IEA project MoSART, and by NCBR Poland & FNR Luxembourg under the PolLux/FNR-CORE project SpaceVote (POLLUXXI/14/SpaceVote/2023). [11] M. Kacprzak and W. Penczek. Unbounded model checking for alternating-time temporal logic. In Proceedings of the 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), pages 646–653, 2004. IEEE Computer Society. [12] M. Kacprzak and W. Penczek. Fully symbolic unbounded model checking for alternatingtime temporal logic. Autonomous Agents and Multi-Agent Systems, 11( 1 ):69–89, 2005. [13] M. Knapik, É. André, L. Petrucci, W. Jamroga, and W. Penczek. Timed ATL: forget memory, just count. Journal of Artificial Intelligence Research , 66:197–223, 2019. [14] F. Laroussinie, N. Markey, and G. Oreiby. Model-Checking Timed ATL for Durational Concurrent Game Structures. In Proceedings of the 4th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2006, volume 4202 of Lecture Notes in Computer Science, pages 245–259, 2006. Springer. [15] A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf., 19( 1 ):9–30, 2017.

References

[1] R. Alur , T. A. Henzinger , and O. Kupferman . Alternating-time Temporal Logic . In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS '97) , pages 100 - 109 , Palo Alto, CA, USA, 1997 . IEEE Computer Society.

[2] R. Alur , T. A. Henzinger , and O. Kupferman . Alternating-time Temporal Logic . Journal of the ACM , 49 : 672 - 713 , 2002 .

[3] É. André. IMITATOR 3: Synthesis of timing parameters beyond decidability . In A. Silva and K. R. M . Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021 , Virtual Event , Proceedings, Part I , volume 12759 of Lecture Notes in Computer Science, pages 552 - 565 . Springer, 2021 .

[4] J. Arias , W. Jamroga , W. Penczek , L. Petrucci , and T. Sidoruk . Strategic (timed) computation tree logic . In N. Agmon, B. An , A. Ricci , and W. Yeoh, editors, Proceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2023 , pages 382 - 390 . ACM, 2023 .

[5] F. Belardinelli , R. Condurache , C. Dima , W. Jamroga , and A. Jones . Bisimulations for verification of strategic abilities with application to ThreeBallot voting protocol . In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS) , pages 1286 - 1295 . IFAAMAS, 2017 .

[6] N. Bulling , J. Dix , and W. Jamroga . Model checking logics of strategic ability: Complexity . In M. Dastani, K. Hindriks , and J.-J. Meyer, editors, Specification and Verification of MultiAgent Systems , pages 125 - 159 . Springer, 2010 .

[7] X. Huang and R. van der Meyden. Symbolic model checking epistemic strategy logic . In Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI14) , pages 1426 - 1432 , Palo Alto, CA, USA, 2014 . AAAI Press.

[8] W. Jamroga , M. Knapik , D. Kurpiewski , and Ł. Mikulski. Approximate verification of strategic abilities under imperfect information . Artificial Intelligence , 277 , 2019 .

[9] W. Jamroga , L. Masko , L. Mikulski , W. Pazderski , W. Penczek , T. Sidoruk , and D. Kurpiewski . Verification of multi-agent properties in electronic voting: A case study . In D. FernándezDuque, A. Palmigiano , and S. Pinchinat, editors, Advances in Modal Logic, AiML 2022 , pages 531 - 556 . College Publications, 2022 .

[10] W. Jamroga , W. Penczek , T. Sidoruk , P. Dembiński , and A. Mazurkiewicz . Timed ATL: forget memory, just count . Journal of Artificial Intelligence Research , 68 : 817 - 850 , 2020 .