Unbounded Model Checking for ATL - Kański, Michał; Niewiadomski, Artur; Kacprzak, Magdalena; Penczek, Wojciech; Nabiałek, Wojciech (Studia Informatica. System and information technology, 2021)
In this paper, we deal with verification of multi-agent systems represented as concurrent game structures. To express properties to be verified, we use Alternating-Time Temporal Logic (ATL) formulas. We provide an implementation of symbolic model checking for ATL and preliminary, but encouraging experimental results.