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.
Coalition Alternating-Time Temporal Logic: A Logic to Find Good Coalitions to Achieve Strategic Objectives / Catta, D.; Ferrando, A.; Malvone, V.. - 14546 LNAI:(2024), pp. 72-94. (Intervento presentato al convegno Agents and Artificial Intelligence: 15th International Conference tenutosi a Lisbon nel February 22-24, 2023) [10.1007/978-3-031-55326-4_4].
Coalition Alternating-Time Temporal Logic: A Logic to Find Good Coalitions to Achieve Strategic Objectives
Ferrando A.;
2024
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.
Pubblicazioni consigliate
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris
