Enqvist and Goranko’s temporal logic of coalitional goal assignments (TL-CGA) extends Alur, Henzinger, and Kupferman’s 1997 alternating-time temporal logic (ATL) and de Pauly’s 2002 coalition logic (CL). TL-CGA is used in multi-agent environments (MAS) and artificial intelligence (AI) to model complex interactions and objectives between agents. This paper focuses on the formalization of CGA, reasoning about coalitions and the development of tools and logical operators for this purpose.
The first extension, that is, TLCGA+, allows for modeling and reasoning about the “sheep and wolves” example. The authors use the concept of Nash equilibria (NE) to analyze the behavior of agents, such as animals facing each other’s challenges within coalitions based on their objectives and strategies. While NE are used to analyze strategic interactions, it is important to note that, typically, animal behavior is not explicitly guided by NE or formal game theory. Instead, animal behavior is often a result of evolutionary pressures and adaptations to their environments.
The second extension, LXCGAμ, which is a logical coalgebraic fixed-point operator in the style of modal µ-calculus, allows reasoning about coalgebraic systems with temporal and fixed-point properties. Applying the extended closure (Fischer-Ladner) TLCGA formula allows for the construction of a modular system, where each module functions with its own well-defined functionality, simplifying system design and maintenance.
Understanding the coalgebraic languages LTLCGA and LXCGAμ is crucial for effectively working with finite action models. These languages are the core of the research and enable reasoning about temporal and coalitional properties.