Parameterised verification for multi-agent systems
File(s)1-s2.0-S0004370216000151-main.pdf (1.38 MB)
Published version
Author(s)
Lomuscio, AR
kouvaros
Type
Journal Article
Abstract
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.
Date Issued
2016-05-01
Date Acceptance
2016-01-13
Citation
Artificial Intelligence, 2016, 234 (4), pp.152-189
ISSN
1872-7921
Publisher
Elsevier
Start Page
152
End Page
189
Journal / Book Title
Artificial Intelligence
Volume
234
Issue
4
Copyright Statement
© 2016 The Authors. Published by Elsevier B.V. This is an open access article under the
CC BY license (http://creativecommons.org/licenses/by/4.0/).
CC BY license (http://creativecommons.org/licenses/by/4.0/).
Copyright URL
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Grant Number
EP/I00520X/1
COLAR_P60375
Subjects
Science & Technology
Technology
Computer Science, Artificial Intelligence
Computer Science
Multi-agent systems
Validation
Parameterised verification
Cutoffs
BOUNDED MODEL CHECKING
KNOWLEDGE
Artificial Intelligence & Image Processing
0801 Artificial Intelligence and Image Processing
0802 Computation Theory and Mathematics
1702 Cognitive Sciences
Publication Status
Published
Date Publish Online
2016-01-18