Skip to Main content Skip to Navigation
New interface
Conference papers

Verifying Strategic Abilities in Multi-agent Systems via First-order Entailment

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.
Complete list of metadata
Contributor : Frédéric Davesne Connect in order to contact the contributor
Submitted on : Tuesday, March 16, 2021 - 1:15:50 AM
Last modification on : Tuesday, January 18, 2022 - 2:26:07 PM
Long-term archiving on: : Thursday, June 17, 2021 - 6:09:38 PM


Files produced by the author(s)


  • HAL Id : hal-03170192, version 1


Francesco Belardinelli, Vadim Malvone. Verifying Strategic Abilities in Multi-agent Systems via First-order Entailment. 24th European Conference on Artificial Intelligence (ECAI 2020), Aug 2020, Santiago de Compostela, Spain. ⟨hal-03170192⟩



Record views


Files downloads