  We present MsATL: the first tool for deciding the satisfiability of
Alternating-time Temporal Logic (ATL) with imperfect information. MsATL
combines SAT Modulo Monotonic Theories solvers with existing ATL model
checkers: MCMAS and STV. The tool can deal with various semantics of ATL,
including perfect and imperfect information, and can handle additional
practical requirements. MsATL can be applied for synthesis of games that
conform to a given specification, with the synthesised game often being
minimal.

Logic in Computer Science;Multiagent Systems