  We present CGAAL, our efficient on-the-fly model checker for alternating-time
temporal logic (ATL) on concurrent game structures (CGS). We present how our
tool encodes ATL as extended dependency graphs with negation edges and employs
the distributed on-the-fly algorithm by Dalsgaard et al. Our tool offers
multiple novel search strategies for the algorithm, including DHS which is
inspired by PageRank and uses the in-degree of configurations as a heuristic,
IHS which estimates instability of assignment values, and LPS which estimates
the distance to a state satisfying the constituent property using linear
programming. CGS are input using our modelling language LCGS, where composition
and synchronisation are easily described. We prove the correctness of our
encoding, and our experiments show that our tool CGAAL is often one to three
orders of magnitude faster than the popular tool PRISM-games on case studies
from PRISM's documentation and among case studies we have developed. In our
evaluation, we also compare and evaluate our search strategies, and find that
our custom search strategies are often significantly faster than the usual
breadth-first and depth-first search strategies.
