Thomas Brihaye, Aline Goeminne
We study multiplayer turn-based timed games with reachability objectives. In particular, we are interested in the notion of subgame perfect equilibrium (SPE). We prove that deciding the constrained existence of an SPE in this setting is EXPTIME-complete.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
We study turn-based quantitative multiplayer non zero-sum games played on finite graphs with reachability objectives. In such games, each player aims at reaching his own goal set of states as soon as possible. A previous work on this model showed that Nash equilibria (resp. secure equilibria) are guaranteed to exist in the multiplayer (resp. two-player) case. The existence of secure equilibria in the multiplayer case remained and is still an open problem. In this paper, we focus our study on the concept of subgame perfect equilibrium, a refinement of Nash equilibrium well-suited in the framewo…
We study $n$-player turn-based games played on a finite directed graph. For each play, the players have to pay a cost that they want to minimize. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. We also study natural variants of SPE, named weak (resp. very weak) SPE, where players who deviate cannot use the full class of strategies but only a subclass with a finite number of (resp. a unique) deviation step(s). Our results are threefold. Firstly, we c…
Weighted timed games are played by two players on a timed automaton equipped with weights: one player wants to minimise the accumulated weight while reaching a target, while the other has an opposite objective. Used in a reactive synthesis perspective, this quantitative extension of timed games allows one to measure the quality of controllers. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. Decidability results exist for subclasses of one-clock games, and for a subclass with non-negative weights defined by a semantical restr…
The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games
本文研究定量可达性博弈中SPE的复杂性，证明约束存在性问题是PSPACE完全的，并提出一种通过迭代约束至不动点来刻画SPE结果集的新算法。
In a reachability-time game, players Min and Max choose moves so that the time to reach a final state in a timed automaton is minimised or maximised, respectively. Asarin and Maler showed decidability of reachability-time games on strongly non-Zeno timed automata using a value iteration algorithm. This paper complements their work by providing a strategy improvement algorithm for the problem. It also generalizes their decidability result because the proposed strategy improvement algorithm solves reachability-time games on all timed automata. The exact computational complexity of solving reacha…
We study two player reachability-price games on single-clock timed automata. The problem is as follows: given a state of the automaton, determine whether the first player can guarantee reaching one of the designated goal locations. If a goal location can be reached then we also want to compute the optimum price of doing so. Our contribution is twofold. First, we develop a theory of cost functions, which provide a comprehensive methodology for the analysis of this problem. This theory allows us to establish our second contribution, an EXPTIME algorithm for computing the optimum reachability pri…
Priced timed games (PTGs) are two-player zero-sum games played on the infinite graph of configurations of priced timed automata where two players take turns to choose transitions in order to optimize cost to reach target states. Bouyer et al. and Alur, Bernadsky, and Madhusudan independently proposed algorithms to solve PTGs with nonnegative prices under certain divergence restriction over prices. Brihaye, Bruyere, and Raskin later provided a justification for such a restriction by showing the undecidability of the optimal strategy synthesis problem in the absence of this divergence restrictio…
Rational verification and checking for Nash and subgame-perfect equilibria in graph games
本文研究图上多人非零和无限持续博弈中的理性检查与验证问题，并给出 Nash 均衡、子博弈完美均衡及五类收益函数下的复杂度。
Permissive Equilibria in Multiplayer Reachability Games
本文研究多人可达性博弈中的多策略，提出用惩罚度量宽容性，并证明在惩罚上界以一元给出时，可在 PSPACE 内判定满足上界约束的纳什均衡或子博弈完美均衡多策略的存在性。
We study multiplayer reachability games played on a finite directed graph equipped with target sets, one for each player. In those reachability games, it is known that there always exists a Nash equilibrium (NE) and a subgame perfect equilibrium (SPE). But sometimes several equilibria may coexist such that in one equilibrium no player reaches his target set whereas in another one several players reach it. It is thus very natural to identify "relevant" equilibria. In this paper, we consider different notions of relevant equilibria including Pareto optimal equilibria and equilibria with high soc…
The Non-Cooperative Rational Synthesis Problem for Subgame Perfect Equilibria and omega-regular Objectives
本文研究了图上多人博弈中遵循子博弈完美均衡的理性合成问题，通过将其编码为不完全信息三人博弈求解，证明该问题在ω-regular目标下属于2ExpTime，并在固定玩家数量等条件下具有更低复杂度。
Verification of Correlated Equilibria in Concurrent Reachability Games
本文研究了并发可达游戏中相关均衡的验证问题，提出子博弈完美相关均衡的概念，并分析了其计算复杂性，发现尽管相关均衡更一般，但其验证问题在标准复杂性假设下更难。
We study multiplayer turn-based games played on a finite directed graph such that each player aims at satisfying an omega-regular Boolean objective. Instead of the well-known notions of Nash equilibrium (NE) and subgame perfect equilibrium (SPE), we focus on the recent notion of weak subgame perfect equilibrium (weak SPE), a refinement of SPE. In this setting, players who deviate can only use the subclass of strategies that differ from the original one on a finite number of histories. We are interested in the constrained existence problem for weak SPEs. We provide a complete characterization o…
Simple Nash Equilibria for Qualitative Multiplayer Games
研究具有ω-正则目标的回合制确定性游戏中纳什均衡和子博弈完美均衡的记忆需求，证明特定目标组合下无记忆随机子博弈完美均衡存在并给出构建算法，指出部分游戏构建无记忆均衡需随机化及其他穆勒目标下不一定存在。
Approximating the Value of Time-Bounded Weighted Timed Games
本文针对执行有时间限制的加权时序博弈，证明其值的近似问题在4-ExpTime复杂度下可判定，解决了该类博弈值问题不可精确计算的困境。
We study multiplayer turn-based games played on a finite directed graph such that each player aims at satisfying an omega-regular Boolean objective. Instead of the well-known notions of Nash equilibrium (NE) and subgame perfect equilibrium (SPE), we focus on the recent notion of weak subgame perfect equilibrium (weak SPE), a refinement of SPE. In this setting, players who deviate can only use the subclass of strategies that differ from the original one on a finite number of histories. We are interested in the constrained existence problem for weak SPEs. We provide a complete characterization o…
(Un)Decidability of Two-Clock Weighted Timed Games
本文证明了使用两个时钟和非负权重的加权时序游戏的价值问题在时间有界条件下仍不可判定，填补了算法理解的最后一个空白。
Reaching as Cheap as Possible in 1-clock Robust Weighted Timed Games
研究鲁棒加权时间博弈中可达性目标的值问题，证明1时钟子类的可判定性，通过构建区域自动机并分析最优策略。
Playing Stochastically in Weighted Timed Games to Emulate Memory
研究加权时间博弈中利用随机决策模拟有限记忆，证明在发散博弈及最短路径博弈中随机值等于确定性值，Min可仅用随机选择保证最优值。
An average-time game is played on the infinite graph of configurations of a finite timed automaton. The two players, Min and Max, construct an infinite run of the automaton by taking turns to perform a timed transition. Player Min wants to minimise the average time per transition and player Max wants to maximise it. A solution of average-time games is presented using a reduction to average-price game on a finite graph. A direct consequence is an elementary proof of determinacy for average-time games. This complements our results for reachability-time games and partially solves a problem posed …
Two-player zero-sum games are a well-established model for synthesising controllers that optimise some performance criterion. In such games one player represents the controller, while the other describes the (adversarial) environment, and controller synthesis corresponds to computing the optimal strategies of the controller for a given criterion. Asarin and Maler initiated the study of quantitative games on (non-probabilistic) timed automata by synthesising controllers which optimise the time to reach a final state. The correctness and termination of their approach was dependent on exploiting …
Synthesis of Robust Optimal Strategies in Weighted Timed Games
本文针对加权时间博弈中时间度量不精确的问题，引入基于扰动的鲁棒语义，通过结合分段仿射函数与收缩差分界矩阵计算鲁棒值函数，首次给出鲁棒值问题的可判定性结果，并证明一般 WTG 的鲁棒可达性为 EXPTIME 完全。
In this paper, we consider reachability games over general hybrid systems, and distinguish between two possible observation frameworks for those games: either the precise dynamics of the system is seen by the players (this is the perfect observation framework), or only the starting point and the delays are known by the players (this is the partial observation framework). In the first more classical framework, we show that time-abstract bisimulation is not adequate for solving this problem, although it is sufficient in the case of timed automata . That is why we consider an other equivalence, n…
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。