论文标题
关于无限并发多人游戏中临时联盟和LTL可定义有序目标的推理
Reasoning about Temporary Coalitions and LTL-definable Ordered Objectives in Infinite Concurrent Multiplayer Games
论文作者
论文摘要
如果在同时的游戏模型上解释,我们建议加强使用命题来表示在时间语言(例如CTL*)中建立的决策和策略。增强功能可以指定不同的联盟结构。在量化的CTL*中,该技术还可以对联盟结构进行量化,我们使用它来量化捕获临时联盟的策略概况的扩展形式。我们还通过二进制优先运算符的时间形式扩展了CTL*,可以追溯到von Wright的工作。量化的CTL*的结果扩展可用于阐明并发多人游戏中行为合理性的条件,例如解决方案概念中出现的内容,并且玩家对其有多个个人目标和偏好,并且有可能形成考虑考虑考虑的临时联盟。我们提出了由时间偏好操作员扩展CTL*的完整公理。逻辑的可决定性不受该扩展的影响。
We propose enhancing the use of propositions for denoting decisions and strategies as established in temporal languages such as CTL*, if interpreted on concurrent game models. The enhancement enables specifying varying coalition structure. In quantified CTL* this technique also enables quantifying over coalition structure, and we use it to quantify over an extended form of strategy profiles which capture temporary coalitions. We also extend CTL* by a temporal form of a binary preference operator that can be traced back to the work of Von Wright. The resulting extension of quantified CTL* can be used to spell out conditions on the rationality of behaviour in concurrent multiplayer games such as what appear in solution concepts, with players having multiple individual objectives and preferences on them, and with the possibility to form temporary coalitions taken in account. We propose complete axiomatisations for the extension of CTL* by the temporal preference operator. The decidability of the logic is not affected by that extension.