Open AccessThe Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games
Author(s) -
Sebastian Enqvist,
Valentin Goranko
Publication year - 2022
Publication title -
acm transactions on computational logic
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.593
H-Index - 52
eISSN - 1557-945X
pISSN - 1529-3785
DOI - 10.1145/3517128
Subject(s) - bisimulation , decidability , axiom , temporal logic , extension (predicate logic) , property (philosophy) , operator (biology) , linear temporal logic , construct (python library) , computer science , mathematics , theoretical computer science , path (computing) , mathematical economics , programming language , philosophy , biochemistry , chemistry , geometry , epistemology , repressor , transcription factor , gene
We introduce and study a natural extension of the Alternating time temporal logic\(\mathsf {ATL} \) , calledTemporal Logic of Coalitional Goal Assignments (TLCGA). It features one new and quite expressive coalitional strategic operator, called thecoalitional goal assignment operator ⟨[γ ]⟩, whereγ is a mapping assigning to each set of players in the game its coalitionalgoal , formalised by a path formula of the language of TLCGA, i.e. a formula prefixed with a temporal operator\(\mathsf {X}, \mathsf {U} \) , or\(\mathsf {G} \) , representing a temporalised objective for the respective coalition, describing the property of the plays on which that objective is satisfied. Then, the formula ⟨[γ ]⟩ intuitively says that there is a strategy profileΣ for the grand coalition\(\operatorname{\mathsf {Agt}} \) such that for each coalitionC , the restrictionΣ |C ofΣ toC is a collective strategy ofC that enforces the satisfaction of its objectiveγ (C ) in all outcome plays enabled byΣ |C .We establish fixpoint characterizations of the temporal goal assignments in aμ -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.