MsATL: a Tool for SAT-Based ATL Satisfiability Checking

in Proceedings of 19th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2020 (2020)

We present MsATL: the first tool for deciding the satisfiability of Alternating-time Temporal Logic ( ATL ) with imperfect informa- tion. MsATL combines SAT Modulo Monotonic Theories solvers with existing ... [more ▼]

We present MsATL: the first tool for deciding the satisfiability of Alternating-time Temporal Logic ( ATL ) with imperfect informa- tion. 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 imper- fect 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. [less ▲]