奇偶对策的延迟升级策略
A Delayed Promotion Policy for Parity Games
摘要：
奇偶博弈是图上的两人无限持续时间博弈，在理论计算机科学的各个领域都起着至关重要的作用。在实践中找到有效的算法来解决这些游戏被广泛认为是形式化验证中的核心问题，因为它导致表达时态逻辑的模型检查和可满足性问题的有效解决方案，例如，modal muCalculus。他们的解决方案可以归结为确定游戏的位置集的问题，称为domestic，在每个位置中，玩家可以通过永远留在集合中来迫使获胜。最近，一种新的技术来计算领域，称为优先级提升，已被提出，这是基于准领域的概念，一个宽松的形式的领域，和领域空间。底层框架足够通用，以适应不同的实例化的解决方案的过程中，其正确性是由空间本身的性质。在本文中，我们提出了一个新的这样的实例，称为延迟推广，试图减少可能的指数行为所表现出的原始方法在最坏的情况下。由此产生的程序不仅往往优于原来的优先级提升方法，但到目前为止，没有指数最坏的情况下是已知的。
英文摘要：
Parity games are two-player infinite-duration games on graphs that play a crucial role in various fields of theoretical computer science. Finding efficient algorithms to solve these games in practice is widely acknowledged as a core problem in formal verification, as it leads to efficient solutions of the model-checking and satisfiability problems of expressive temporal logics, e.g., the modal muCalculus. Their solution can be reduced to the problem of identifying sets of positions of the game, called dominions, in each of which a player can force a win by remaining in the set forever. Recently, a novel technique to compute dominions, called priority promotion, has been proposed, which is based on the notions of quasi dominion, a relaxed form of dominion, and dominion space. The underlying framework is general enough to accommodate different instantiations of the solution procedure, whose correctness is ensured by the nature of the space itself. In this paper we propose a new such instantiation, called delayed promotion, that tries to reduce the possible exponential behaviours exhibited by the original method in the worst case. The resulting procedure not only often outperforms the original priority promotion approach, but so far no exponential worst case is known.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
