TY - CPAPER AB - We introduce an abstraction methodology for the verificationof multi-agent systems against specifications expressed inalternating-time temporal logic (ATL). Inspired by methodolo-gies such as predicate abstraction, we define a three-valuedsemantics for the interpretation of ATL formulas on concurrentgame structures and compare it to the standard two-valued se-mantics. We define abstract models and establish preservationresults on the three-valued semantics between abstract modelsand their concrete counterparts. We illustrate the methodologyon the large state spaces resulting from a card game. AU - Lomuscio,AR EP - 437 PB - AAAI Press PY - 2014/// SP - 428 TI - An abstraction technique for the verification of multi-agent systems against ATL specifications UR - http://www.aaai.org/Press/Proceedings/kr14.php UR - http://hdl.handle.net/10044/1/26814 ER -