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 cor- responding model checking problems. Most importantly, we show that the three-valued semantics constitutes an approxi- mation with respect to the traditional two-valued semantics. In the light of this we construct a sound, albeit partial, al- gorithm for model checking two-valued perfect recall via its approximation as three-valued bounded recall