In this paper, we present CGAAL, our model checker of alternating-time temporal logic properties in concurrent games.

To evaluate our tool, we run several experiments. In our experiments we compare our global algorithm, our local algorithm using our various search strategies

The syntax of the language is inspired by PRISM-lang used by the PRISM model checker to model stochastic multi-player games with rewards.

In order to check if a CGS satisfies an ATL property, CGAAL encodes the problem as an extended dependency graph and finds a fixed-point assignment