@inproceedings{dd6b2c9ccb6046e285a6640a99be378a,
title = "Coalition Alternating-Time Temporal Logic: A Logic to Find Good Coalitions to Achieve Strategic Objectives",
abstract = "Alternating-time Temporal Logic (ATL) extends the temporal logic CTL, permitting quantification over coalitions of agents. During the model checking process, the coalitions defined in a given formula are predetermined, operating under the assumption that the user possesses knowledge about the specific coalitions under exam. However, this presumption is not universally applicable. The outcome of this paper is twofold. Initially, we introduce CATL, a modified version of ATL which empowers users to define coalition quantifiers based on two key attributes: the number of agents involved within the coalitions and the methodology for grouping these agents. Subsequently, we show the incorporation of CATL into MCMAS, a widely recognized tool dedicated to ATL model checking. Additionally, we provide details of this extension accompanied by empirical experiments.",
keywords = "Alternating-time Temporal logic, Coalition of agents, Formal verification, Logics for strategic reasoning",
author = "Davide Catta and Angelo Ferrando and Vadim Malvone",
note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.; 15th International Conference on Agents and Artificial Intelligence, ICAART 2023 ; Conference date: 22-02-2023 Through 24-02-2023",
year = "2024",
month = jan,
day = "1",
doi = "10.1007/978-3-031-55326-4\_4",
language = "English",
isbn = "9783031553257",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "72--94",
editor = "Rocha, \{Ana Paula\} and Luc Steels and \{van den Herik\}, Jaap",
booktitle = "Agents and Artificial Intelligence - 15th International Conference, ICAART 2023, Revised Selected Papers",
}