We introduce an abstraction methodology for the verification
of multi-agent systems against specifications expressed in
alternating-time temporal logic (ATL). Inspired by methodolo-
gies such as predicate abstraction, we define a three-valued
semantics for the interpretation of ATL formulas on concurrent
game structures and compare it to the standard two-valued se-
mantics. We define abstract models and establish preservation
results on the three-valued semantics between abstract models
and their concrete counterparts. We illustrate the methodology
on the large state spaces resulting from a card game.