Playing Games with Boxes and Diamonds
Playing Games with Boxes and Diamonds
复制标题
用盒子和钻石玩游戏
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
P. Madhusudan
中科院分区：
文献类型：
--
作者：
R. Alur;S. L. Torre;P. Madhusudan
在有限图上确定无线电图的无限图，已知由线性逻辑（LTL）公式指定的，已知使用下一个和/或直到操作员，已知已知的硬度证明是2 expime-collette。此外，在模型检查的情况下，将接下来的且只能保留始终，有时是操作员，从而降低了从Pspace到NP的复杂性确定游戏的复杂性可能是一个开放的问题。总是有时是运算符，我们还可以证明，如果在此片段中，我们不允许有时的操作员在始终操作员的范围内，而是决定游戏是扩展的，与以前已知的上限相匹配。 P，然后可以在PSPACE中确定游戏，还可以建立匹配的下限。
Deciding infinite two-player games on finite graphs with the winning condition specified by a linear temporal logic (Ltl) formula, is known to be 2Exptime-complete. The previously known hardness proofs encode Turing machine computations using the next and/or until operators. Furthermore, in the case of model checking, disallowing next and until, and retaining only the always and eventually operators, lowers the complexity from Pspace to Np. Whether such a reduction in complexity is possible for deciding games has been an open problem. In this paper, we provide a negative answer to this question. We introduce new techniques for encoding Turing machine computations using games, and show that deciding games for the Ltl fragment with only the always and eventually operators is 2Exptime-hard. We also prove- that if in this fragment we do not allow the eventually operator in the scope of the always operator and vice-versa, deciding games is Expspace-hard, matching the previously known upper bound. On the positive side, we show that if the winning condition is a Boolean combination of formulas of the form “eventually p” and “infinitely often p,” for a state-formula p, then the game can be decided in Pspace, and also establish a matching lower bound. Such conditions include safety and reachability specifications on game graphs augmented with fairness conditions for the two players.