Scalable verification of strategy logic through three-valued abstraction
File(s)3___valued_SL-1.pdf (353.08 KB)
Accepted version
Author(s)
Belardinelli, F
Ferrando, A
Jamroga, W
Malvone, V
Murano, A
Type
Conference Paper
Abstract
The model checking problem for multi-agent systems against Strategy Logic specifications is known to be non-elementary. On this logic several fragments have been defined to tackle this issue but at the expense of expressiveness. In this paper, we propose a three-valued semantics for Strategy Logic upon which we define an abstraction method. We show that the latter semantics is an approximation of the classic two-valued one for Strategy Logic. Furthermore, we extend MCMAS, an open-source model checker for multi-agent specifications, to incorporate our abstraction method and present some promising experimental results.
Date Acceptance
2023-08-19
Citation
IJCAI : proceedings of the conference / sponsored by the International Joint Conferences on Artificial Intelligence, 2023-August, pp.46-54
ISBN
9781956792034
ISSN
1045-0823
Publisher
International Joint Conference on Artificial Intelligence
Start Page
46
End Page
54
Journal / Book Title
IJCAI : proceedings of the conference / sponsored by the International Joint Conferences on Artificial Intelligence
Volume
2023-August
Copyright Statement
Copyright © 2023 International Joint Conferences on Artificial Intelligence
Identifier
https://www.ijcai.org/proceedings/2023/6
Source
32nd International Joint Conference on Artificial Intelligence
Publication Status
Published
Start Date
2023-08-19
Finish Date
2023-08-25
Coverage Spatial
Macao, SAR
Date Publish Online
2023-08-19