Faster Solutions of Rabin and Streett Games
Faster Solutions of Rabin and Streett Games
复制标题
Rabin 和 Streett Games 的更快解决方案
DOI：
10.1109/lics.2006.23
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
A. Pnueli
中科院分区：
文献类型：
--
作者：
Nir Piterman;A. Pnueli
在本文中，我们提高了解决Rabin和Streett游戏的复杂性，以大约是以前界限的平方根。我们介绍了直接的Rabin和StreetT排名，这是描述各自游戏中获胜场景的一种健全和完整的方式。通过直接和明确计算排名，我们可以在时间o（mnk+1kk！）和space o（nk）的rabin和o（nkk！）的空间o（nk！）中解决此类游戏，其中n是状态的数量，m的过渡次数和k在获胜条件下的成对数。为了证明排名方法的完整性，我们给出了这些游戏中获胜区域的递归fixpoint表征。然后，我们表明，通过在FixPoint评估期间保持中间值，我们可以在时间O（NK+1K！）和Space O（NK+1K！）中象征性地解决此类游戏。在直接（符号）解决方案或O（m（nk2k！）k）的情况下，这些结果会改善O（MN2KK！）时间的当前界限
In this paper we improve the complexity of solving Rabin and Streett games to approximately the square root of previous bounds. We introduce direct Rabin and Streett ranking that are a sound and complete way to characterize the winning sets in the respective games. By computing directly and explicitly the ranking we can solve such games in time O(mnk+1kk!) and space O(nk) for Rabin and O(nkk!) for Streett where n is the number of states, m the number of transitions, and k the number of pairs in the winning condition. In order to prove completeness of the ranking method we give a recursive fixpoint characterization of the winning regions in these games. We then show that by keeping intermediate values during the fixpoint evaluation, we can solve such games symbolically in time O(nk+1k!) and space O(nk+1k!). These results improve on the current bounds of O(mn2kk!) time in the case of direct (symbolic) solution or O(m(nk2k!)k) in the case of reduction to parity games