Approximate Verification of Strategic Abilities Under Imperfect Information Using Local Models
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.
Cite
Text
Kurpiewski et al. "Approximate Verification of Strategic Abilities Under Imperfect Information Using Local Models." International Joint Conference on Artificial Intelligence, 2025. doi:10.24963/IJCAI.2025/17Markdown
[Kurpiewski et al. "Approximate Verification of Strategic Abilities Under Imperfect Information Using Local Models." International Joint Conference on Artificial Intelligence, 2025.](https://mlanthology.org/ijcai/2025/kurpiewski2025ijcai-approximate/) doi:10.24963/IJCAI.2025/17BibTeX
@inproceedings{kurpiewski2025ijcai-approximate,
title = {{Approximate Verification of Strategic Abilities Under Imperfect Information Using Local Models}},
author = {Kurpiewski, Damian and Jamroga, Wojciech and Kim, Yan},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2025},
pages = {143-151},
doi = {10.24963/IJCAI.2025/17},
url = {https://mlanthology.org/ijcai/2025/kurpiewski2025ijcai-approximate/}
}