AAAI Publications, Sixteenth International Conference on Principles of Knowledge Representation and Reasoning

Font Size: 
Approximating Perfect Recall When Model Checking Strategic Abilities
Francesco Belardinelli, Alessio Lomuscio, Vadim Malvone

Last modified: 2018-11-26


We investigate the notion of bounded recall in the context of model checking ATL* and ATL specifications in multi-agent systems with imperfect information.  We present a novel three-valued semantics for ATL*, respectively ATL, under bounded recall and imperfect information, and study the corresponding model checking problems. Most importantly, we show that the three-valued semantics constitutes an approximation with respect to the traditional two-valued semantics. In the light of this we construct a sound, albeit partial, algorithm for model checking two-valued perfect recall via its approximation as three-valued bounded recall.


Alternating-time Temporal Logic; Model Checking; Verification of Multi-Agent Systems

Full Text: PDF