Skip to Main content Skip to Navigation
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

https://hal.archives-ouvertes.fr/hal-03170192
Contributor : Frédéric Davesne <>
Submitted on : Tuesday, March 16, 2021 - 1:15:50 AM
Last modification on : Thursday, July 1, 2021 - 11:04:07 AM
Long-term archiving on: : Thursday, June 17, 2021 - 6:09:38 PM

File

ECAI2020_FB_VM.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03170192, version 1

Citation

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⟩

Share

Metrics

Record views

31

Files downloads

15