Skip to Main content Skip to Navigation
New interface
Journal articles

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.
Complete list of metadata

https://hal.telecom-paris.fr/hal-03779030
Contributor : Vadim Malvone Connect in order to contact the contributor
Submitted on : Friday, September 16, 2022 - 1:34:44 PM
Last modification on : Thursday, November 10, 2022 - 4:06:23 AM

Links full text

Identifiers

Citation

Francesco Belardinelli, Alessio Lomuscio, Vadim Malvone, Emily Yu. Approximating Perfect Recall when Model Checking Strategic Abilities: Theory and Applications. Journal of Artificial Intelligence Research, 2022, 73, pp.897-932. ⟨10.1613/jair.1.12539⟩. ⟨hal-03779030⟩

Share

Metrics

Record views

18