Unbounded model checking for alternating-time temporal logic

This paper deals with the problem of verification of game-like structures by means of symbolic model checking. Alternating-time Temporal Logic (ATL) is used for expressing properties of multi-agent systems represented by concurrent game structures. Unbounded model checking (a SAT based technique) is applied for the first time for verification of ATL. An example is given to show an application of the technique.