The temporal logic of coalitional goal assignments in concurrent multi-player games

TL;DR

This paper introduces TLCGA, an extension of ATL with a coalitional goal assignment operator, providing a formal framework for reasoning about coalitional strategies and goals in multi-player games.

Contribution

It presents a new logical framework with a novel operator, fixpoint characterizations, and a complete axiomatic system for analyzing coalitional goals in concurrent games.

Findings

Establishes fixpoint characterizations of goal assignments.

Proves bisimulation invariance and Hennessy-Milner property.

Provides a sound and complete axiomatic system with decidability.

Abstract

We introduce and study a natural extension of the Alternating time temporal logic ATL, called Temporal Logic of Coalitional Goal Assignments (TLCGA). It features just one, but quite expressive, coalitional strategic operator, viz. the coalitional goal assignment operator, which is based on a mapping assigning to each set of players in the game its coalitional goal, formalised by a path formula of the language of TLCGA, i.e. a formula prefixed with a temporal operator X,U, or G, representing a temporalised objective for the respective coalition, describing the property of the plays on which that objective is satisfied. We establish fixpoint characterizations of the temporal goal assignments in a mu-calculus extension of TLCGA, discuss its expressiveness and illustrate it with some examples, prove bisimulation invariance and Hennessy-Milner property for it with respect to a suitably defined notion of bisimulation, construct a sound and complete axiomatic system for TLCGA, and obtain its decidability via finite model property.