Abstract
We provide a symbolic algorithm for synthesizing winning strategies in Alternating Time Temporal Logic. ATL has game semantics, which makes it suitable for modelling open systems where coalitions of agents work together to achieve their goals. A typical use of the algorithm would begin with a highly non-deterministic set of agents, A, for which we wish to synthesize behaviour. These may be composed with a set of opponent agents, which provide an environment. The desired behaviour is then written in \left\langle {\left\langle A \right\rangle } \right\rangle-LTL, and a strategy for A to implement this is synthesised. If A implements this strategy, then the system will be guaranteed to satisfy the desired property. The algorithm presented here is part of a work in progress and updates can be found at http://www.cs. bham.ac.uk/~ath/atl_synthesis.