Imperial College London

ProfessorAlessioLomuscio

Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems
 
 
 
//

Contact

 

+44 (0)20 7594 8414a.lomuscio Website

 
 
//

Location

 

504Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Kouvaros:2013,
author = {Kouvaros, P and Lomuscio, A},
journal = {12th International Conference on Autonomous Agents and Multiagent Systems 2013, AAMAS 2013},
pages = {861--868},
title = {Automatic verification of parameterised interleaved multi-agent systems},
volume = {2},
year = {2013}
}

RIS format (EndNote, RefMan)

TY  - JOUR
AB - A key problem in verification of multi-agent systems by model checking concerns the fact that the state-space of the system grows exponentially with the number of agents present. This often makes practical model checking unfeasible whenever the system contains more than a few agents. In this paper we put forward a technique to establish a cutoff result, thereby showing that systems with an arbitrary number of agents can be verified by checking a single system consisting of a number of agents equal to the cutoff of the system. While this problem is undecidable in general, we here define a class of parameterised interpreted systems and a parameterised temporal-epistemic logic for which the result can be shown. We exemplify the theoretical results on a robotic example and present an implementation of the technique as an extension of MCMAS, an open-source model checker for multi-agent systems. Copyright © 2013, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
AU - Kouvaros,P
AU - Lomuscio,A
EP - 868
PY - 2013///
SP - 861
TI - Automatic verification of parameterised interleaved multi-agent systems
T2 - 12th International Conference on Autonomous Agents and Multiagent Systems 2013, AAMAS 2013
VL - 2
ER -