An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information
File(s)
Accepted version
Author(s)
Belardinelli, Francesco
Ferrando, Angelo
Malvone, Vadim
Type
Journal Article
Abstract
We investigate the verification of Multi-Agent Systems against strategic properties expressed in Alternating-time Temporal Logic under the assumptions of imperfect information and perfect recall. To this end, we develop a three-valued semantics for concurrent game structures upon which we define an abstraction method. We prove that concurrent game structures with imperfect information admit perfect information abstractions that preserve three-valued satisfaction. Furthermore, to deal with cases in which the value of a specification is undefined, we develop a novel automata-theoretic technique for the linear-time logic (LTL), then apply it to finding “failure” states. The latter can then be fed into a refinement procedure, thus providing a sound, albeit incomplete, verification method. We illustrate the overall procedure in a variant of the Train Gate Controller scenario and a simple voting protocol under imperfect information and perfect recall. We also present an implementation of our procedure and provide preliminary experimental results.
Date Issued
2023-03
Date Acceptance
2022-12-24
Citation
Artificial Intelligence, 2023, 316
ISSN
0004-3702
Publisher
Elsevier BV
Journal / Book Title
Artificial Intelligence
Volume
316
Copyright Statement
Copyright © Elsevier Ltd. All rights reserved. This manuscript version is made available under the CC-BY-NC-ND 4.0 license https://creativecommons.org/licenses/by-nc-nd/4.0/
Identifier
http://dx.doi.org/10.1016/j.artint.2022.103847
Publication Status
Published
Article Number
103847
Date Publish Online
2023-01-05