Publications

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}
}

Download

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  -

Download

ProfessorAlessioLomuscio

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)