Verifying strategic abilities in multi-agent systems via first-order entailment
File(s) FAIA-325-FAIA200072.pdf (329.82 KB)
Published version
Author(s)
Belardinelli, F
Malvone, V
Type
Conference Paper
Abstract
The verification of strategic abilities of autonomous agents is a key subject of investigation in the applications of formal methods to the design and certification of multi-agents systems. In this contribution we propose a novel approach to this verification problem. Inspired by recent advances, we introduce a translation from Alternating-time Temporal Logic (ATL) to First-order Logic (FOL). We show that our translation is sound on a fragment of ATL, that we call ATL-live, as it is suitable to express liveness properties in MAS. Further, we show how the universal model checking problem for ATL-live can be reduced to semantic entailment in FOL. Finally, we prove that ATL-live is maximal in the sense that if any other ATL connective is added, non-FOL reasoning techniques would be required. These results are meant to be a first step towards the application of FOL reasoners to model check strategic abilities expressed in ATL.
Date Issued
2020-08-24
Date Acceptance
2020-08-29
Citation
Frontiers in Artificial Intelligence and Applications, 2020, 325, pp.27-34
ISBN
9781643681009
ISSN
0922-6389
Publisher
IOS Press
Start Page
27
End Page
34
Journal / Book Title
Frontiers in Artificial Intelligence and Applications
Volume
325
Copyright Statement
© 2020 The authors and IOS Press.
This article is published online with Open Access by IOS Press and distributed under the terms
of the Creative Commons Attribution Non-Commercial License 4.0 (CC BY-NC 4.0).
This article is published online with Open Access by IOS Press and distributed under the terms
of the Creative Commons Attribution Non-Commercial License 4.0 (CC BY-NC 4.0).
License URL
Identifier
https://ebooks.iospress.nl/publication/54867
Source
24th European Conference on Artificial Intelligence
Publication Status
Published
Start Date
2020-08-29
Finish Date
2020-09-08
Coverage Spatial
Santiago de Compostela, Spain
Date Publish Online
2020
