Title: Abstraction for model checking modular interpreted systems over ATL
Abstract: We propose an abstraction technique for model checking multi-agent systems given as modular interpreted systems (MIS) which allow for succinct representations of compositional systems. Specifications are given as arbitrary ATL formulae, i. e., we can reason about strategic abilities of groups of agents. Our technique is based on collapsing each agent's local state space with hand-crafted equivalence relations, one per strategic modality. We develop 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.
Publication Year: 2011
Publication Date: 2011-05-02
Language: en
Type: article
Access and Citation
Cited By Count: 10
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot