Abstraction for Model Checking Modular Interpreted Systems over ATL

摘要

We present an abstraction technique for model checking multi-agent systems given as modular interpreted systems (MIS) (introduced by Jamroga and Agotnes). MIS allow for succinct representations of compositional systems, they permit agents to be removed, added or replaced and they are modular by facilitating control over the amount of interaction. Specifications are given as arbitrary ATL formulae: We can therefore reason about strategic abilities of groups of agents. Our technique is based on collapsing each agent's local state space with handcrafted equivalence relations, one per strategic modality. We present a model checking algorithm and prove its soundness: This makes it possible to perform model checking on abstractions (which are much smaller in size) rather than on the concrete system which is usually too complex, thereby saving space and time. We illustrate our technique with an example in a scenario of autonomous agents exchanging information.