SAT-Based ATL Satisfiability Checking

Synthesis of models and strategies is a very important task in software engineering. The main problem here consists in checking the satisfiability of formulae expressing the specification of a system to be implemented. This paper puts forward a novel method for deciding the satisfiability of formulae of Alternating-time Temporal Logic (ATL) under perfect and imperfect information. The synthesised models of strategic games are often minimal. The method expands the one for CTL exploiting SAT Modulo Monotonic Theories (SMMT) solvers. Our tool MsATL combines SMMT solvers with two existing ATL model checkers: MCMAS and STV. This is the first ever tool for checking the satisfiability of imperfect information ATL. The experimental results show that, similarly to the CTL case, our approach appears to be very efficient and can quickly check the satisfiability of large ATL formulae that have been out of reach of the existing approaches.