MsATL: a Tool for SAT-Based ATL Satisfiability Checking

TL;DR

MsATL is a novel tool that leverages SAT solvers and existing ATL model checkers to decide satisfiability of ATL formulas under various semantics, including imperfect information, enabling practical synthesis applications.

Contribution

It introduces the first SAT-based approach for ATL satisfiability checking that supports imperfect information and integrates with existing model checkers.

Findings

Successfully handles ATL with imperfect information

Supports various ATL semantics including perfect and imperfect information

Enables synthesis of minimal conforming games

Abstract

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.