An abstraction technique for the verification of multi-agent systems against ATL specifications
Alessio R. Lomuscio, Jakub Michaliszyn · 2014
We introduce an abstraction methodology for the verification of multi-agent systems against specifications expressed in alternating-time temporal logic (ATL). Inspired by methodolo-gies such as predicate abstraction, we define a three-valued semantics for the interpretation of ATL formulas on concurrent game structures and compare it to the standard two-valued se-mantics. We define abstract models and establish preservation results on the three-valued semantics between abstract models and their concrete counterparts. We illustrate the methodology on the large state spaces resulting from a card game. 1