6 results found
Lomuscio AR, kouvaros, 2016, Parameterised verification for multi-agent systems, Artificial Intelligence, Vol: 234, Pages: 152-189, ISSN: 1872-7921
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.
Lomuscio AR, Kouvaros P, 2015, Verifying Emergent Properties of Swarms, Twenty-Fourth International Conference on Artificial Intelligence (IJCAI15), Publisher: AAAI Press, Pages: 1083-1089
Lomuscio AR, Kouvaros P, 2015, A counter abstraction technique for the verification of robot swarms., Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI15), Publisher: AAAI, Pages: 2081-2088
We study parameterised verification of robot swarms against temporal-epistemic specifications. We relax some of the significant restrictions assumed in the literature and present a counter abstraction approach that enable us to verify a potentially much smaller abstract model when checking a formula on a swarm of any size. We present an implementation and discuss experimental results obtained for the alpha algorithm for robot swarms.
Kouvaros P, Lomuscio A, 2013, A cutoff technique for the verification of parameterised interpreted systems with parameterised environments, Twenty-Third Joint Conference on Artificial Intelligence, Publisher: AAAI Press / International Joint Conferences on Artificial Intelligence, Pages: 2013-2019, ISSN: 1045-0823
We put forward a cutoff technique for determining the number of agents that is sufficient to consider when checking temporal-epistemic specifications on a system of any size. We identify a special class of interleaved interpreted systems for which we give a parameterised semantics and an abstraction methodology. This enables us to overcome the significant limitations in expressivity present in the state-of-the-art. We present an implementation and discuss experimental results.
Kouvaros P, Lomuscio A, 2013, Automatic verification of parameterised interleaved multi-agent systems, 12th International Conference on Autonomous Agents and Multiagent Systems 2013, AAMAS 2013, Vol: 2, Pages: 861-868
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.
Kouvaros P, Lomuscio A, 2013, Automatic verification of parameterised multi-agent systems., Publisher: IFAAMAS, Pages: 861-868
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.