The temporal logic of coalitional goal assignments in
concurrent multi-player games
Valentin Goranko
Stockholm University
Abstract:
I will present the recently introduced Temporal Logic of Coalitional
Goal Assignments (TLCGA), which is a natural extension of the
Alternating time temporal logic ATL. TLCGA features just one, but
quite expressive, coalitional strategic operator, called “coalitional
goal assignment operator”. It is based on a mapping assigning to each
set (coalition) of players in the game its coalitional goal,
formalised by a path formula of the language of TLCGA representing a
temporalised objective for the respective coalition describing the
property of the plays on which that objective is satisfied.
I will illustrate the use of the logic TLCGA with some examples. In
particular, I will introduce the new solution concept of
“co-equilibrium”, which is particularly suitable for multi-player
games with qualitative coalitional objectives, and will show that it
can be naturally expressed in TLCGA.
Time permitting, I will then briefly outline our main technical
results for that logic, including: fixpoint characterizations of the
temporal goal assignment operators in a mu-calculus extension of
TLCGA, bisimulation invariance and Hennessy-Milner property with
respect to a suitably defined notion of bisimulation; a sound and
complete axiomatic system, and decidability of satisfiability via
finite model property.
The talk will be relatively self-contained, though it will assume
some general background on temporal logics in computer science.
The talk is based on the following paper:
Sebastian Enqvist and Valentin Goranko,
The temporal logic of coalitional goal assignments in concurrent
multi-player games.
ACM Transactions of Computational Logic, Vol. 23, No. 4, Article 21,
2022.
Available from:
https://link.springer.com/article/10.1007/s10458-021-09531-9