Approximate verification; Imperfect information; Imperfect recall; Artificial Intelligence; Model checking
Abstract :
[en] Verification of strategic ability under imperfect information is challenging, with complexity ranging from NP-complete to undecidable. This is partly because traditional fixpoint equivalences fail in this setting. Some years ago, an interesting idea of fixpoint approximation was proposed for model checking of ATLir, i.e., the logic of strategic ability for agents with imperfect information and imperfect recall. In this paper, we propose a new variant of the approximation, that uses the agent's local model rather than the global model of the system. We prove correctness of the construction, and demonstrate its effectiveness through experimental results on scalable models of voting.
Disciplines :
Computer science
Author, co-author :
Kurpiewski, Damian; Institute of Computer Science, Polish Academy of Sciences, Poland ; Nicolaus Copernicus University, Toruń, Poland
Jamroga, Wojciech; Institute of Computer Science, Polish Academy of Sciences, Poland ; Nicolaus Copernicus University, Toruń, Poland
Approximate Verification of Strategic Abilities under Imperfect Information Using Local Models
Publication date :
2025
Event name :
Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence
Event place :
Montreal, Canada
Event date :
16-08-2025 => 22-08-2025
Main work title :
Proceedings of the 34th International Joint Conference on Artificial Intelligence, IJCAI 2025
Editor :
Kwok, James
Publisher :
International Joint Conferences on Artificial Intelligence
ISBN/EAN :
978-1-956792-06-5
Peer reviewed :
Peer reviewed
FnR Project :
FNR17232062 - SpaceVote - Probabilistic Verification Of Complex Heterogeneous Systems: From Ballots To Ballistics, 2022 (01/03/2023-28/02/2026) - Peter Y. A. Ryan
Funders :
International Joint Conferences on Artifical Intelligence (IJCAI)
Funding text :
The work has been supported by NCBR Poland and FNR Luxembourg under the PolLux/FNR-CORE project SpaceVote (POLLUX-XI/14/SpaceVote/2023 and C22/IS/17232062/SpaceVote). For the purpose of open access, and in fulfilment of the grant agreement, the authors have applied CC BY 4.0 license to any Author Accepted Manuscript version arising from this submission.
Rajeev Alur, Thomas Henzinger, Freddy Y.C. Mang, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran. MOCHA: Modularity in model checking. In Proceedings of Computer Aided Verification (CAV), volume 1427 of Lecture Notes in Computer Science, pages 521-525. Springer, 1998.
R. Alur, L. de Alfaro, R. Grossu, T.A. Henzinger, M. Kang, C.M. Kirsch, R. Majumdar, F.Y.C. Mang, and B.-Y. Wang. jMocha: A model-checking tool that exploits design structure. In Proceedings of International Conference on Software Engineering (ICSE), pages 835-836. IEEE Computer Society Press, 2001.
Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time Temporal Logic. Journal of the ACM, 49:672-713, 2002.
Edward A Ashcroft. Proving assertions about parallel programs. Journal of Computer and System Sciences, 10(1):110-135, 1975.
G. Behrmann, A. David, and K.G. Larsen. A tutorial on UPPAAL. In Formal Methods for the Design of Real-Time Systems: SFM-RT, number 3185 in LNCS, pages 200-236. Springer, 2004.
Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, and Sasha Rubin. Verification of broadcasting multi-agent systems against an epistemic strategy logic. In Proceedings of IJCAI, pages 91-97, 2017.
R. Berthon, B. Maubert, A. Murano, S. Rubin, and M. Y. Vardi. Strategy logic with imperfect information. In Proceedings of LICS, pages 1-12, 2017.
N. Bulling and W. Jamroga. Alternating epistemic mu-calculus. In Proceedings of IJCAI-11, pages 109-114, 2011.
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 Multi-Agent Systems, pages 125-159. Springer, 2010.
Simon Busard, Charles Pecheur, Hongyang Qu, and Franco Raimondi. Improving the model checking of strategies under partial observability and fairness constraints. In Formal Methods and Software Engineering, volume 8829 of Lecture Notes in Computer Science, pages 27-42. Springer, 2014.
Simon Busard, Charles Pecheur, Hongyang Qu, and Franco Raimondi. Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. Information and Computation, 242:128-156, 2015.
Petr Cermak, Alessio Lomuscio, Fabio Mogavero, and Aniello Murano. MCMAS-SLK: A model checker for the verification of strategy logic specifications. In Proc. of Computer Aided Verification (CAV), volume 8559 of Lecture Notes in Computer Science, pages 525-532. Springer, 2014.
Petr Cermák, Alessio Lomuscio, and Aniello Murano. Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In Proceedings of AAAI, pages 2038-2044, 2015.
Taolue Chen, Vojtech Forejt, Marta Kwiatkowska, David Parker, and Aistis Simaitis. PRISM-games: A model checker for stochastic multi-player games. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 7795 of Lecture Notes in Computer Science, pages 185-191. Springer, 2013.
Catalin Dima and Ferucio L. Tiplea. Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225, 2011.
Dimitar P. Guelev, Catalin Dima, and Constantin Enea. An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking. Journal of Applied Non-Classical Logics, 21(1):93-131, 2011.
Xiaowei Huang and Ron van der Meyden. Symbolic model checking epistemic strategy logic. In Proceedings of AAAI Conference on Artificial Intelligence, pages 1426-1432, 2014.
Wojciech Jamroga, Michał Knapik, Damian Kurpiewski, and Łukasz Mikulski. Approximate verification of strategic abilities under imperfect information. Artificial Intelligence, 277, 2019.
W. Jamroga, W. Penczek, T. Sidoruk, P. Dembiński, and A. Mazurkiewicz. Towards partial order reductions for strategic ability. Journal of Artificial Intelligence Research, 68:817-850, 2020.
Wojciech Jamroga, Yan Kim, Damian Kurpiewski, and Peter Y. A. Ryan. Towards model checking of voting protocols in uppaal. In Proceedings of E-Vote-ID, volume 12455 of Lecture Notes in Computer Science, pages 129-146. Springer, 2020.
Wojciech Jamroga, Wojciech Penczek, and Teofil Sidoruk. Strategic abilities of asynchronous agents: Semantic side effects and how to tame them. In Proceedings of KR 2021, pages 368-378, 2021.
M. Kacprzak and W. Penczek. Unbounded model checking for alternating-time temporal logic. In Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 646-653. IEEE Computer Society, 2004.
Mateusz Kaminski, Damian Kurpiewski, and Wojciech Jamroga. STV+KH: towards practical verification of strategic ability for knowledge and information flow. In Proceedings of AAMAS, pages 2812-2814. ACM, 2024.
Yan Kim, Wojciech Jamroga, and Peter Y.A. Ryan. Verification of the socio-technical aspects of voting: The case of the Polish postal vote 2020. In Proceedings of STAST, 2022. To appear, available at https://arxiv.org/abs/2210.10694.
Damian Kurpiewski, Wojciech Jamroga, and Michał Knapik. STV: Model checking for strategies under imperfect information. In Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019, pages 2372-2374. IFAAMAS, 2019.
Damian Kurpiewski, Witold Pazderski, Wojciech Jamroga, and Yan Kim. STV+Reductions: Towards practical verification of strategic ability using model reductions. In Proceedings of AAMAS, pages 1770-1772. ACM, 2021.
Damian Kurpiewski, Wojciech Jamroga, Lukasz Masko, Lukasz Mikulski, Witold Pazderski, Wojciech Penczek, and Teofil Sidoruk. Verification of multi-agent properties in electronic voting: A case study. In Advances in Modal Logic, pages 531-556. College Publications, 2022.
Damian Kurpiewski, Wojciech Jamroga, and Teofil Sidoruk. Towards modelling and verification of social explainable AI. In Proceedings of ICAART, pages 396-403, 2023.
Damian Kurpiewski, Mateusz Kamiński, Yan Kim, Łukasz Maśko, Witold Pazderski, Wojciech Jamroga, and Łukasz Mikulski. STV - StraTegic Verifier. code repository, 2024. https://github.com/blackbat13/stvv2.
A. Lomuscio and F. Raimondi. MCMAS: A model checker for multi-agent systems. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 4314 of Lecture Notes in Computer Science, pages 450-454. Springer, 2006.
Alessio Lomuscio, Hongyang Qu, and Franco Raimondi. MCMAS: An open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer, 19(1):9-30, 2017.
F. Mogavero, A. Murano, and M.Y. Vardi. Reasoning about strategies. In Proceedings of FSTTCS, pages 133-144, 2010.
Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic, 15(4):1-42, 2014.
J. Pilecki, M.A. Bednarczyk, and W. Jamroga. Synthesis and verification of uniform strategies for multi-agent systems. In Proceedings of CLIMA XV, volume 8624 of Lecture Notes in Computer Science, pages 166-182. Springer, 2014.
Pierre-Yves Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2):82-93, 2004.
