TY - GEN
T1 - Coalition Alternating-Time Temporal Logic
T2 - 15th International Conference on Agents and Artificial Intelligence, ICAART 2023
AU - Catta, Davide
AU - Ferrando, Angelo
AU - Malvone, Vadim
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2024.
PY - 2024/1/1
Y1 - 2024/1/1
N2 - 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.
AB - 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.
KW - Alternating-time Temporal logic
KW - Coalition of agents
KW - Formal verification
KW - Logics for strategic reasoning
UR - https://www.scopus.com/pages/publications/85189552442
U2 - 10.1007/978-3-031-55326-4_4
DO - 10.1007/978-3-031-55326-4_4
M3 - Conference contribution
AN - SCOPUS:85189552442
SN - 9783031553257
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 72
EP - 94
BT - Agents and Artificial Intelligence - 15th International Conference, ICAART 2023, Revised Selected Papers
A2 - Rocha, Ana Paula
A2 - Steels, Luc
A2 - van den Herik, Jaap
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 22 February 2023 through 24 February 2023
ER -