Solving Games Without Determinization
Solving Games Without Determinization
复制标题
在没有确定性的情况下解决博弈
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Nir Piterman
中科院分区：
文献类型：
--
作者：
T. Henzinger;Nir Piterman
反应系统的综合需要求解具有ω-正则目标的图上的二人博弈。当目标由线性时态逻辑公式或非确定性Buchi自动机指定时，以前求解游戏的算法需要构造等效的确定性自动机。然而，确定性的自动机上无限的话是非常复杂的，目前的实现未能产生确定性的自动机，即使是相对较小的输入。我们展示了如何从一个给定的不确定性Buchi自动机，一个等价的不确定性奇偶自动机$\ensuremath {\cal P}$，这是很好的解决游戏的目标$\ensuremath {\cal P}$。主要的见解是，一个非确定性自动机是好的解决游戏，如果它公平地模拟等效的确定性自动机。通过这种方式，我们省略了博弈求解和反应合成中的确定步骤。我们的自动机是不确定的，这一事实使它们非常简单，易于符号实现，并允许对获胜策略进行增量搜索。
The synthesis of reactive systems requires the solution of two-player games on graphs with ω-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Buchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Buchi automaton, an equivalent nondeterministic parity automaton $\ensuremath {\cal P}$ that is good for solving games with objective $\ensuremath {\cal P}$. The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows an incremental search for winning strategies.