We investigate the verification of Multi-agent Systems
against strategic properties expressed in Alternating-time
Temporal Logic under the assumptions of imperfect informa-
tion and perfect recall. To this end, we develop a three-valued
semantics for concurrent game structures upon which we de-
fine an abstraction method. We prove that concurrent game
structures with imperfect information admit perfect informa-
tion abstractions that preserve three-valued satisfaction. Fur-
ther, we present a refinement procedure to deal with cases
where the value of a specification is undefined. We illustrate
the overall procedure in a variant of the Train Gate Controller
scenario under imperfect information and perfect recall.