A counter abstraction technique for verifying properties of probabilistic swarm systems
File(s)
Accepted version
Author(s)
Lomuscio, Alessio
Pirovano, Edoardo
Type
Journal Article
Abstract
We introduce a semantics for reasoning about probabilistic multi-agent systems in which the number of participants is not known at design-time. We define the parameterised model checking problem against PLTL specifications for this semantics, and observe that this is undecidable in general. Nonetheless, we develop a partial decision procedure for it based on counter abstraction. We prove the correctness of this procedure, and present an implementation of it. We then use our implementation to verify a number of example scenarios from swarm robotics and other settings.
Date Issued
2022-04
Date Acceptance
2022-01-20
Citation
Artificial Intelligence, 2022, 305, pp.103666-103666
ISSN
0004-3702
Publisher
Elsevier BV
Start Page
103666
End Page
103666
Journal / Book Title
Artificial Intelligence
Volume
305
Copyright Statement
© 2022 Elsevier B.V. All rights reserved.
Sponsor
Royal Academy Of Engineering
Identifier
http://sciencedirect.com/science/article/pii/S0004370222000066?via%3Dihub
Grant Number
CIET 1718/26
Subjects
Artificial Intelligence & Image Processing
0801 Artificial Intelligence and Image Processing
0802 Computation Theory and Mathematics
1702 Cognitive Sciences
Publication Status
Published online
Article Number
103666
Date Publish Online
2022-01-24