论文标题
具有LDL目标有限痕迹的多游戏游戏
Multi-Player Games with LDL Goals over Finite Traces
论文作者
论文摘要
有限轨迹上的线性动态逻辑LDLF是一种强大的逻辑，用于推理并发和多代理系统的行为。 在本文中，我们研究了多玩游戏游戏中表征和验证的技术，其目标/目标是使用基于LDLF的逻辑表达的目标。这项研究以布尔游戏的概括为基础，这是一种基于逻辑的多代理系统的游戏模型，玩家的目标以逻辑方式简洁地代表。 由于考虑了LDLF目标，因此在我们研究的设置中 - 反应性模块游戏和具有有限痕迹的目标的迭代布尔游戏 - 玩家的目标可以定义为有限但任意较大的痕迹的同时实现的定期属性。 特别是，使用交替的自动机，该论文研究了（纯策略NASH）平衡的表征和验证的自动机理论方法，表明具有LDLF目标的多游戏游戏中NASH均衡的集合是规则的，并为相关的自动组合结构提供了复杂性结果。
Linear Dynamic Logic on finite traces LDLf is a powerful logic for reasoning about the behaviour of concurrent and multi-agent systems. In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using logics based on LDLf. This study builds upon a generalisation of Boolean games, a logic-based game model of multi-agent systems where players have goals succinctly represented in a logical way. Because LDLf goals are considered, in the settings we study -- Reactive Modules games and iterated Boolean games with goals over finite traces -- players' goals can be defined to be regular properties while achieved in a finite, but arbitrarily large, trace. In particular, using alternating automata, the paper investigates automata-theoretic approaches to the characterisation and verification of (pure strategy Nash) equilibria, shows that the set of Nash equilibria in multi-player games with LDLf objectives is regular, and provides complexity results for the associated automata constructions.
