论文标题
符合符号平价游戏的即时解决
On-The-Fly Solving for Symbolic Parity Games
论文作者
论文摘要
奇偶游戏可用于表示许多不同类型的决策问题。实际上，使用平价游戏的工具通常依赖于高阶逻辑中的规范，可以通过探索从中获得实际游戏。对于许多这些决策问题，我们只对游戏中指定的顶点的解决方案感兴趣。我们正式化了如何在探索过程中使用自然解决的技术，并表明这可以有助于在不完整的游戏中确定此类指定顶点的获胜者。此外，我们为不完整的平等游戏定义了部分求解技术，并显示如何使这些技术直接在不完整的游戏中直接工作，而不是在一组安全的顶点上工作。我们为符号平价游戏实施我们的技术，并在实践中研究它们的有效性，表明多个数量级的加速是可行的，开销（如果不可避免的话）通常很低。
Parity games can be used to represent many different kinds of decision problems. In practice, tools that use parity games often rely on a specification in a higher-order logic from which the actual game can be obtained by means of an exploration. For many of these decision problems we are only interested in the solution for a designated vertex in the game. We formalise how to use on-the-fly solving techniques during the exploration process, and show that this can help to decide the winner of such a designated vertex in an incomplete game. Furthermore, we define partial solving techniques for incomplete parity games and show how these can be made resilient to work directly on the incomplete game, rather than on a set of safe vertices. We implement our techniques for symbolic parity games and study their effectiveness in practice, showing that speed-ups of several orders of magnitude are feasible and overhead (if unavoidable) is typically low.
