随机BPA对策的定性可达性

Qualitative Planning in Imperfect Information Games with Active Sensing and Reactive Sensor Attacks: Cost of Unawareness

We consider the probabilistic planning problem where the agent (called Player 1, or P1) can jointly plan the control actions and sensor queries in a sensor network and an attacker (called player 2, or P2) can carry out attacks on the sensors. We model such an adversarial interaction using a formal model -- a reachability game with partially controllable observation functions. The main contribution of this paper is to assess the cost of P1's unawareness: Suppose P1 misinterprets the sensor failures as probabilistic node failures due to unreliable network communication, and P2 is aware of P1's m…

超越获胜策略：定量可达性博弈中的可采纳策略与可采纳获胜策略

Beyond Winning Strategies: Admissible and Admissible Winning Strategies for Quantitative Reachability Games

本文研究定量可达性博弈中的可采纳策略与可采纳获胜策略，证明其历史依赖性和存在性条件，提出综合算法，并在网格世界和机器人机械臂场景中验证。

无限持续期Poorman投标博弈

Infinite-Duration Poorman-Bidding Games

在图上的双人游戏中，玩家在图中移动令牌以产生无限路径，这决定了游戏的赢家或收益。这样的游戏是形式化验证的核心，因为它们模拟了非终止系统与其环境之间的交互。我们研究{ \em投标游戏}，其中玩家投标移动令牌的权利。两个投标规则已经确定。在{ \em Richman}出价中，在每一轮中，玩家同时提交出价，出价较高的玩家移动代币并向另一个玩家支付。{ \em Poorman}出价与此类似，只是出价的获胜者支付“银行”而不是其他玩家。虽然Poorman可达性游戏已经研究过，我们目前，第一次，{ \em无限持续时间} Poorman游戏的结果。这些游戏中的一个中心量是两个玩家的初始预算之间的{ \em比率}。我们研究的问题涉及一个玩家能够达到目标的必要和充分比率。对于可达性目标，这样的{ \em阈值比率}已知对于两个竞价规则都存在。我们表明，穷人的可达性游戏的属性扩展到复杂的定性目标，如奇偶校验，类似于里奇曼的情况下。我们最有趣的结果涉及定量poorman游戏，即poorman平均支付游戏，我们根据初始比率构建最优策略，通过显示与{ \em random-turn based games}的连接。这种联系本身就很有趣，因为它不适用于可达性Poorman游戏。我们还解决了poorman投标游戏中出现的复杂性问题。

同时平均支付对策的定性分析

Qualitative Analysis of Concurrent Mean-payoff Games

我们考虑有限状态图上两个玩家的并发博弈，在每一轮中玩家同时选择一个动作，当前状态和联合动作决定了后继状态。我们研究一个基本目标，即平均收益目标，其中奖励与每个过渡相关联，玩家1的目标是最大化长期平均奖励，玩家2的目标是严格相反的。参与人1的路径约束可以是定性的，即，平均回报是最大回报，或者任意接近它;或者是定量的，即，最小和最大奖励之间的给定阈值。我们考虑的计算几乎肯定（resp。正的）获胜集，其中参与者1可以确保路径约束以概率1（分别地，正概率）。我们对定性路径约束的主要结果如下：（1）我们建立了定性确定性结果，表明对于每个状态，任一参与人1都有一个策略来确保几乎确定（分别是）。积极的）战胜所有参与人2的策略，或者参与人2有一个破坏策略来伪造几乎肯定的（分别是积极的）赢得对所有玩家1的战略;（2）我们提出了最佳的战略复杂性的结果，精确地描述了几乎肯定和积极赢得双方球员所需的战略类;和（3）我们提出了二次时间算法来计算几乎肯定和积极的胜利集，匹配最好的已知的边界算法更简单的问题（如可达性目标）。对于定量约束，我们表明，一个多项式时间的解决方案，几乎肯定或积极的获胜集将意味着一个长期存在的开放问题的解决方案（基于回合的确定性平均支付游戏的价值问题），这是不知道是可解的多项式时间。

不精确偏差下终端报酬并发对策的随机均衡

Stochastic Equilibria under Imprecise Deviations in Terminal-Reward Concurrent Games

我们研究了图上的并发博弈中混合策略均衡的存在性。虽然每个玩家的安全目标保证了纳什均衡的存在性，但当玩家被赋予任意的最终奖励目标时，纳什均衡不需要存在，并且它们的存在性对于定性的可达性目标是不可判定的（并且只有三个玩家）。然而，这些结果依赖于这样一个事实，即参与者可以在试图提高他们的收益的同时实施无限的游戏。在本文中，我们介绍了一个宽松的概念，平衡，偏差是不精确的。我们证明，相反的纳什均衡，这样的（固定）平衡总是存在的，我们开发了一个PSPACE算法来计算。

Reaching Your Goal Optimally by Playing at Random

Shortest-path games are two-player zero-sum games played on a graph equipped with integer weights. One player, that we call Min, wants to reach a target set of states while minimising the total weight, and the other one has an antagonistic objective. This combination of a qualitative reachability objective and a quantitative total-payoff objective is one of the simplest setting where Min needs memory (pseudo-polynomial in the weights) to play optimally. In this article, we aim at studying a tradeoff allowing Min to play at random, but using no memory. We show that Min can achieve the same opti…

不完全信息下的定性并发随机对策

Qualitative Concurrent Stochastic Games with Imperfect Information

我们研究了一个模型的游戏，结合并发性，不完美的信息和随机方面。这些是有限状态博弈，在每一轮中，两个参与者同时独立地选择一个行动。然后，根据前一个状态和参与者选择的一对行动，根据某个固定的概率分布来选择后继状态。不完全信息模型如下：两个玩家在状态上有一个等价关系，而不是观察确切的状态，他们只知道它属于哪个等价类。因此，如果某个参与者无法区分两种局部策略，那么他在这两种策略中的行为应该是相同的。我们考虑可达性（戏剧最终会访问最终状态吗？）和Büchi目标（是否发挥访问无限经常一个最终状态？）。我们的主要贡献是证明了以下问题是2-ExpTime完全的：决定第一个玩家是否有一个策略，确保她几乎肯定会赢得任何可能的策略，她oponent。我们还讨论了第一个几乎肯定会赢的玩家所需要的策略。

无共享随机性的团队博弈中的极限确定获胜

Limit-sure Winning in Team Games without Shared Randomness

本文研究无共享随机性的团队并发随机博弈，针对可达性目标证明极限确定问题为NP完全，安全性目标下极限确定获胜等价于几乎确定获胜，还得出Individually Randomised ATL定性片段模型检测为P^NP完全的结论。

具有折扣和长期平均目标的随机对策的放大镜抽象

Magnifying Lens Abstraction for Stochastic Games with Discounted and Long-run Average Objectives

回合制随机博弈及其重要子类马尔可夫决策过程（MDP）为具有概率和非确定性行为的系统提供了模型。我们考虑两个经典的定量目标：折扣和长期平均目标的回合制随机博弈。博弈模型和定量目标在概率验证、规划、最优库存控制、网络协议和性能分析等方面有着广泛的应用。模拟现实系统的游戏和MDP通常具有非常大的状态空间，并且概率抽象技术是处理状态空间爆炸所必需的。通常使用的全抽象技术不产生节省空间的系统，有许多状态具有类似的值，但不一定有类似的过渡结构。提出了一种半抽象技术，即放大镜抽象（MLA），聚类状态的基础上的价值，无视其过渡关系的差异，提出了定性目标（可达性和安全性目标）。在本文中，我们扩展的MLA技术，以解决随机游戏的折扣和长期平均目标。我们提出了基于MLA技术的随机博弈和折扣和目标MDP的抽象-精化算法。对于长期平均目标，我们的解决方案适用于所有MDP和一类随机游戏，其中每个状态具有相同的值。

并发随机有损信道博弈

Concurrent Stochastic Lossy Channel Games

本文提出并发随机有损信道博弈（CSLCG）框架，研究无界有损信道通信下概率多智能体系统的理性验证，证明几乎必然LTL目标下该问题不可判定，并给出涵盖几乎必然可达性与安全性的可判定片段，是无限竞技场上随机多智能体系统理性验证的首个可判定性结果。

多人离散出价博弈：确定性、均衡性与复杂性

Multi-Player Discrete-Bidding Games; Determinacy, Equilibria, and Complexity

本文研究多人离散出价博弈，证明其在温和假设下具有确定性，均值收益博弈存在值，定性博弈存在纯纳什均衡，且可达性博弈中判断联盟获胜的问题为PSPACE-hard。

平均收益下推博弈

Mean-Payoff Pushdown Games

图上的二人博弈是形式化验证和程序分析中许多问题的核心，如开放系统的综合和验证。在这项工作中，我们考虑解决递归游戏图（或下推游戏图），可以模拟顺序程序的控制流与递归。虽然下推游戏已经研究了定性的目标，如可达性和$ω$ -定期的目标，在这项工作中，我们研究了第一次这样的游戏，最好的研究定量目标，即平均回报目标。在下推博弈中，有两种策略是相关的：（1）全局策略，它依赖于整个全局历史;（2）模块策略，它只有局部记忆，因此不依赖于调用的上下文，而只依赖于当前模块调用的历史。主要结果如下：（1）在全局策略下，具有平均支付目标的一人下推对策是多项式时间可判定的。(2)在全局策略下，具有平均支付目标的两人下推博弈是不可判定的。(3)模块化策略下具有平均收益目标的单人下推博弈是NP难的。(4)在模块化策略下具有平均收益目标的两人下推博弈可以在NP中求解（即，在模块化策略下，具有平均收益目标的单人和双人下推博弈都是NP完全的）。我们还建立了最优策略的复杂性表明，平均回报目标的全球战略需要无限的记忆，即使在一个球员的下推游戏和无记忆的模块化策略是足够的两个球员的下推游戏。最后，我们还表明，所有的问题都有相同的复杂性，如果堆栈有界性条件，随着平均回报目标的球员也必须确保堆栈高度有界。

无限期竞价博弈

Infinite-Duration Bidding Games

图上的二人游戏在形式化方法中得到了广泛的研究，因为它们模拟了系统与环境之间的交互。游戏通过在整个图中移动代币来产生无限路径来进行。有几种常见的模式来确定玩家如何在图中移动代币;例如，在基于回合的游戏中，玩家在移动代币时交替回合。我们研究了移动令牌的{ \em出价}模式，据我们所知，这在无限持续时间的游戏中从未被研究过。下面的竞价规则是以前定义的，称为Richman竞价。两个参与者都有单独的{ \em预算}，合计为$1$。在每一轮中，都会发生一次出价：两个玩家同时提交出价，如果出价不超过可用预算，则出价是合法的，出价更高的出价者向另一个玩家支付他的出价并移动代币。竞价博弈中研究的中心问题是赢得博弈的必要且充分的初始预算：顶点中的{ \em阈值}预算是一个值$t \in [0,1]$，使得如果参与者$1$的预算超过$t$，他可以赢得博弈，如果参与者$2$的预算超过$1-t$，他可以赢得博弈。阈值预算以前被证明存在于可达性博弈的每个顶点，这与{ \em random-turn}博弈有一个有趣的联系-一个简单的随机博弈的子类，其中移动的玩家是随机选择的。我们证明了存在的阈值预算的定性类的无限持续时间的游戏，即平价游戏，和定量类，即平均收益游戏。证明的关键组成部分是一个定量的解决方案，强连接的平均支付投标游戏中，我们扩展与随机回合游戏这些游戏的连接，并构建明确的最优策略，为双方球员。