  In logics for the strategic reasoning the main challenge is represented by
their verification in contexts of imperfect information and perfect recall. In
this work, we show a technique to approximate the verification of
Alternating-time Temporal Logic (ATL*) under imperfect information and perfect
recall, which is known to be undecidable. Given a model M and a formula
$\varphi$, we propose a verification procedure that generates sub-models of M
in which each sub-model M' satisfies a sub-formula $\varphi'$ of $\varphi$ and
the verification of $\varphi'$ in M' is decidable. Then, we use CTL* model
checking to provide a verification result of $\varphi$ on M. We prove that our
procedure is in the same class of complexity of ATL* model checking under
perfect information and perfect recall, we present a tool that implements our
procedure, and provide experimental results.
