An abstraction technique for the verification of multi-agent systems against ATL specifications

Copyright © 2014, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.We introduce an abstraction methodology for the verification of multi-agent systems against specifications expressed in alternating-time temporal logic (ATL). Inspired by methodologies 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 semantics. 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