@inproceedings{e23d8b8e14124fd48c0d7530c5756260,
title = "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.",
author = "Francesco Belardinelli and Vadim Malvone",
note = "Publisher Copyright: {\textcopyright} 2020 The authors and IOS Press.; 24th European Conference on Artificial Intelligence, ECAI 2020, including 10th Conference on Prestigious Applications of Artificial Intelligence, PAIS 2020 ; Conference date: 29-08-2020 Through 08-09-2020",
year = "2020",
month = aug,
day = "24",
doi = "10.3233/FAIA200072",
language = "English",
series = "Frontiers in Artificial Intelligence and Applications",
publisher = "IOS Press BV",
pages = "27--34",
editor = "\{De Giacomo\}, Giuseppe and Alejandro Catala and Bistra Dilkina and Michela Milano and Senen Barro and Alberto Bugarin and Jerome Lang",
booktitle = "ECAI 2020 - 24th European Conference on Artificial Intelligence, including 10th Conference on Prestigious Applications of Artificial Intelligence, PAIS 2020 - Proceedings",
}