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.

翻译：我们提出MsATL：首个用于判定含不完美信息交替时态逻辑（ATL）可满足性的工具。MsATL将SAT模单调理论求解器与现有ATL模型检测器MCMAS和STV相结合。该工具可处理ATL的多种语义（包括完美信息与不完美信息），并支持额外的实际需求。MsATL可用于生成符合给定规格的博弈，且所生成的博弈通常具有最小化特征。