Practical verification of multi-agent systems against Slk specifications
File(s)
Accepted version
Author(s)
Čermák, Petr
Lomuscio, Alessio
Mogavero, Fabio
Murano, Aniello
Type
Journal Article
Abstract
We introduce Strategy Logic with Knowledge, a novel formalism to reason about knowledge and strategic ability in memoryless multi-agent systems with incomplete information. We exemplify its expressive power; we define the model checking problem for the logic and show that it is PSpace-complete. We propose a labelling algorithm for solving the verification problem that we show is amenable to symbolic implementation. We introduce Image 1, an extension of the open-source model checker MCMAS, implementing the proposed algorithm. We report the benchmarks obtained on a number of scenarios from the literature, including the dining cryptographers protocol.
Date Issued
2018-08
Date Acceptance
2017-09-01
Citation
Information and Computation, 2018, 261 (Part 3), pp.588-614
ISSN
0890-5401
Publisher
Elsevier BV
Start Page
588
End Page
614
Journal / Book Title
Information and Computation
Volume
261
Issue
Part 3
Copyright Statement
© 2017 Elsevier Ltd. All rights reserved. This manuscript is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International Licence http://creativecommons.org/licenses/by-nc-nd/4.0/
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Grant Number
EP/I00520X/1
Subjects
08 Information And Computing Sciences
Computation Theory & Mathematics
Publication Status
Published
Date Publish Online
2017-09-17