Open AccessApproximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications
Author(s) -
Francesco Belardinelli,
Alessio Lomuscio,
Vadim Malvone,
Emily Yu
Publication year - 2022
Publication title -
journal of artificial intelligence research/the journal of artificial intelligence research
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.79
H-Index - 123
eISSN - 1943-5037
pISSN - 1076-9757
DOI - 10.1613/jair.1.12539
Subject(s) - undecidable problem , bounded function , model checking , recall , semantics (computer science) , computer science , perfect information , theoretical computer science , algorithm , decidability , mathematics , programming language , mathematical economics , mathematical analysis , linguistics , philosophy
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.