Sciweavers

ATAL
2009
Springer

Abstraction in model checking multi-agent systems

13 years 9 months ago
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 ...
Mika Cohen, Mads Dam, Alessio Lomuscio, Francesco
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where ATAL
Authors Mika Cohen, Mads Dam, Alessio Lomuscio, Francesco Russo
Comments (0)