Abstraction is a key technique for reasoning about systems with very large or even infinite state spaces. When a system is composed of reactive components, the interaction between the components is modeled by a multi-player game and verification corresponds to finding winners in the game. We describe an abstraction-refinement framework for multiplayer games, with respect to specifications in the alternating ?-calculus (AMC). Our framework is based on abstract alternating transition systems (AATSs). Each agent in an AATS has transitions that over-approximate its power and transitions that under-approximate its power. We define the framework, define a 3-valued semantics for AMC formulas in an AATS, study the model-checking problem, define an abstraction preorder between AATSs, suggest a refinement procedure (in case model checking returns an indefinite answer), and study the completeness of the framework. For the case of predicate abstraction, we show how reasoning can be automated with a theorem prover.

Abstractions of multi-player games have been studied in the past. Our main contribution with respect to earlier work is that we study general (rather than only turn-based) ATSs, we add a refinement procedure on top of the model checking procedure, and our abstraction preorder is parameterized by a set of agents.