Approximating perfect recall when model checking strategic abilities

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.