Francesco Belardinelli, Alessio Lomuscio, Vadim Malvone, Zhengqi Yu,
"Approximating Perfect Recall When Model Checking Strategic Abilities: Theory and Applications"
, in Journal of Artificial Intelligence Research, Vol. 73, AI Access Foundation, Seite(n) 897-932, 5-2022, ISSN: 1076-9757
Original Titel:
Approximating Perfect Recall When Model Checking Strategic Abilities: Theory and Applications
Sprache des Titels:
Englisch
Original Kurzfassung:
The model checking problem for multi-agent systems against specifications in the alternating-time temporal logic ATL, hence ATL\ast, 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 ATL\ast 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 ATL and other agent specifications, to incorporate bounded recall; we illustrate its use and present experimental results.