Proceedings

Approximate Verification of Strategic Abilities under Imperfect Information Using Local Models

Damian Kurpiewski, Wojciech Jamroga, Yan Kim

Download BibTeX Cite

Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 143-151.

https://doi.org/10.24963/ijcai.2025/17

Keywords

  • Agent-based and Multi-agent Systems: MAS: Formal verification, validation and synthesis

Abstract

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 ATL_ir, 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.

Damian Kurpiewski, Wojciech Jamroga, and Yan Kim. 2025. Approximate Verification of Strategic Abilities under Imperfect Information Using Local Models. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-25. IJCAI, 143–151. https://doi.org/10.24963/ijcai.2025/17
Welcome Future Conferences AI Journal Division IJCAI Proceedings About IJCAI IJCAI Awards