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.