论文标题
Stackelberg-Pareto合成（扩展版）
Stackelberg-Pareto Synthesis (Extended Version)
论文作者
论文摘要
我们研究了在图表上播放的两名玩家Stackelberg游戏的框架，在该图表中，玩家0宣布策略，玩家1通过一种最佳响应的策略做出合理的响应。虽然通常假定玩家1具有一个目标，但我们在这里考虑他有几个目标。在这种情况下，在响应他的策略之后，玩家1以与他满意的目标相对应的布尔人的形式获得了回报。球员1的合理性是由以下事实编码：他的反应必须在策略0的策略下产生帕累托最佳的回报。我们研究了几种$ω$的目标，即Stackelberg-pareto综合问题，该问题能够询问玩家0是否可以满足其目标的策略，无论是否满足他的目标，我们都可以证明自己的目标。安全，Büchi，Co-Büchi，BooleanBüchi，Parity，Muller，Streett或Rabin目标。我们还表明，此问题是Nexptime-Complete，除了Büchi目标的情况下，它是NP完整的，并且在Nexptime和NP-Hard中为此。在简单的可及性目标和图表的简单情况下，该问题已经完成了。
We study the framework of two-player Stackelberg games played on graphs in which Player 0 announces a strategy and Player 1 responds rationally with a strategy that is an optimal response. While it is usually assumed that Player 1 has a single objective, we consider here the new setting where he has several. In this context, after responding with his strategy, Player 1 gets a payoff in the form of a vector of Booleans corresponding to his satisfied objectives. Rationality of Player 1 is encoded by the fact that his response must produce a Pareto-optimal payoff given the strategy of Player 0. We study for several kinds of $ω$-regular objectives the Stackelberg-Pareto Synthesis problem which asks whether Player 0 can announce a strategy which satisfies his objective, whatever the rational response of Player 1. We show that this problem is fixed-parameter tractable for games in which objectives are all reachability, safety, Büchi, co-Büchi, Boolean Büchi, parity, Muller, Streett or Rabin objectives. We also show that this problem is NEXPTIME-complete except for the cases of Büchi objectives for which it is NP-complete and co-Büchi objectives for which it is in NEXPTIME and NP-hard. The problem is already NP-complete in the simple case of reachability objectives and graphs that are trees.
