Abstraction in model checking multi-agent systems

ion in model checking multi-agent systems Mika Cohen Department of Computing Imperial College London London, UK Mads Dam Access Linnaeus Center Royal Institute of Technology Stockholm, Sweden Alessio Lomuscio Department of Computing Imperial College London London, UK Francesco Russo Department of Computing Imperial College London London, UK We present an abstraction technique for multi-agent systems preserving temporal-epistemic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic cation holds on the abstract system, the specification also holds on the concrete one. In principle this permits us check the abstract system rather than the concrete one, thereby saving time and space in the verification step. trate the abstraction technique ...

• Type: Conference
• Year: 2009
• Where: ATAL
• Authors: Mika Cohen, Mads Dam, Alessio Lomuscio, Francesco Russo
• Keywords: Abstraction Technique, Artificial Intelligence, ATAL 2009, Imperial College London, Multi-agent System