  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.
