论文标题
联合多玩家游戏中联盟目标分配的时间逻辑
The temporal logic of coalitional goal assignments in concurrent multi-player games
论文作者
论文摘要
我们介绍并研究了交替时间的时间逻辑ATL的自然扩展，称为联盟目标分配的时间逻辑（TLCGA）。它仅具有一个但表现力的联盟战略运营商，即。联盟目标分配操作员基于映射分配给游戏中的每组玩家的联盟目标，并由TLCGA语言的路径公式形式化，即一个临时操作员x，u或g的公式，代表了对各自的联盟的暂时性目标，描述了该目标的属性。我们在TLCGA的MU-Calculus扩展中建立了固定目标分配的固定点特征，讨论其表现力并用一些示例来说明它，证明了双性模拟不变性和轩尼诗 - 米尔纳属性，相对于合适的符合性概念的概念，可以通过合理定义的符合性概念来构建声音和完整的tlcga属性。
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.
