Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems



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




504Huxley BuildingSouth Kensington Campus






BibTex format

author = {Lomuscio, AR and kouvaros},
doi = {10.1016/j.artint.2016.01.008},
journal = {Artificial Intelligence},
pages = {152--189},
title = {Parameterised verification for multi-agent systems},
url = {},
volume = {234},
year = {2016}

RIS format (EndNote, RefMan)

AB - We study the problem of verifying role-based multi-agent systems, where the number of components cannot be determined at design time. We give a semantics that captures parameterised, generic multi-agent systems and identify three notable classes that represent different ways in which the agents may interact among themselves and with the environment. While the verification problem is undecidable in general we put forward cutoff procedures for the classes identified. The methodology is based on the existence of a notion of simulation between the templates for the agents and the template for the environment in the system. We show that the cutoff identification procedures as well as the general algorithms that we propose are sound; for one class we show the decidability of the verification problem and present a complete cutoff procedure. We report experimental results obtained on MCMAS-P, a novel model checker implementing the parameterised model checking methodologies here devised.
AU - Lomuscio,AR
AU - kouvaros
DO - 10.1016/j.artint.2016.01.008
EP - 189
PY - 2016///
SN - 1872-7921
SP - 152
TI - Parameterised verification for multi-agent systems
T2 - Artificial Intelligence
UR -
UR -
VL - 234
ER -