Formal Verification of Opinion Formation in Swarms
File(s)
Accepted version
Author(s)
Kouvaros, P
Lomuscio, A
Type
Conference Paper
Abstract
We investigate the formal verification of consensus protocols in swarm systems composed of arbitrary many agents. We use templates to define the behaviour of the agents in an opinion dynamics setting and formulate their verification in terms of the associated parameterised model checking problem. We define a finite abstract model that we show to simulate swarms of any size, thereby precisely encoding any concrete instantiation of the swarm. We give an automatic procedure for verifying temporal-epistemic properties of consensus protocols by model checking the associated finite abstract model. We present a toolkit that can be used to generate the abstract model automatically and verify a given protocol by symbolic model checking. We use the toolkit to verify the correctness of majority rule protocols in arbitrary large swarms.
Date Issued
2016-05-09
Date Acceptance
2016-05-09
Citation
Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS '16), 2016, pp.1200-1208
ISBN
978-1-4503-4239-1
Publisher
ACM
Start Page
1200
End Page
1208
Journal / Book Title
Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS '16)
Copyright Statement
© 2016 International Foundation for Autonomous Agents and Multiagent Systems. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems.
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Grant Number
EP/I00520X/1
COLAR_P60375
Source
2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS '16)
Publication Status
Published
Start Date
2016-05-09
Finish Date
2016-05-13
Coverage Spatial
Singapore