Approximating Perfect Recall When Model Checking Strategic Abilities: Theory and Applications
Abstract
The model checking problem for multi-agent systems against specifications in the alternating-time temporal logic AT L, hence AT L∗ , under perfect recall and imperfect information is known to be undecidable. To tackle this problem, in this paper we investigate a notion of bounded recall under incomplete information. We present a novel three-valued semantics for AT L∗ in this setting and analyse the corresponding model checking problem. We show that the three-valued semantics here introduced is an approximation of the classic two-valued semantics, then give a sound, albeit partial, algorithm for model checking two-valued perfect recall via its approximation as three-valued bounded recall. Finally, we extend MCMAS, an open-source model checker for AT L and other agent specifications, to incorporate bounded recall; we illustrate its use and present experimental results.
Cite
Text
Belardinelli et al. "Approximating Perfect Recall When Model Checking Strategic Abilities: Theory and Applications." Journal of Artificial Intelligence Research, 2022. doi:10.1613/JAIR.1.12539Markdown
[Belardinelli et al. "Approximating Perfect Recall When Model Checking Strategic Abilities: Theory and Applications." Journal of Artificial Intelligence Research, 2022.](https://mlanthology.org/jair/2022/belardinelli2022jair-approximating/) doi:10.1613/JAIR.1.12539BibTeX
@article{belardinelli2022jair-approximating,
title = {{Approximating Perfect Recall When Model Checking Strategic Abilities: Theory and Applications}},
author = {Belardinelli, Francesco and Lomuscio, Alessio and Malvone, Vadim and Yu, Emily},
journal = {Journal of Artificial Intelligence Research},
year = {2022},
pages = {897-932},
doi = {10.1613/JAIR.1.12539},
volume = {73},
url = {https://mlanthology.org/jair/2022/belardinelli2022jair-approximating/}
}