AAAI Publications, Fourteenth International Conference on the Principles of Knowledge Representation and Reasoning

Font Size: 
An Abstraction Technique for the Verification of Multi-Agent Systems Against ATL Specifications
Alessio Lomuscio, Jakub Michaliszyn

Last modified: 2014-05-04


We introduce an abstraction methodology for the verification ofmulti-agent systems against specifications expressed in alternating-timetemporal logic (ATL). Inspired by methodologies such as predicateabstraction, we define a three-valued semantics for the interpretationof ATL formulas on concurrent game structures and compare it to thestandard two-valued semantics. We define abstract models and establishpreservation results on the three-valued semantics between abstractmodels and their concrete counterparts. We illustrate the methodologyon the large state spaces resulting from a card game.

Full Text: PDF