Speaker: Valentin Goranko
Date and Time: Thursday, March 11th 2021, 16:30-18:00, Amsterdam time.
Venue: online.
Title: The temporal logic of coalitional goal assignments in concurrent multi-player games.
Abstract. I will present 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, 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 (like in ATL) 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 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.
This is joint work with Sebastian Enqvist, available here. See here for the recording of the talk.