Effective partial solvers for parity games 1
Effective partial solvers for parity games 1
复制标题
奇偶博弈的有效部分求解器 1
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
M. Huth
中科院分区：
文献类型：
--
作者：
Patrick Ah;M. Huth
部分方法在形式方法和其他方法中起着重要的作用。最近，这种方法被开发的奇偶校验游戏，多项式时间部分求解器决定一个子集的节点的赢家。我们在这里调查如何有效的多项式时间部分求解器可以在原则上通过研究多项式时间的相互作用的部分求解器。具体地说，我们提出了简单的，通用的组成模式，部分求解器，保持多项式时间的可计算性。我们表明，这个语义框架的实现手动发现新的部分求解器-包括那些合并节点集，具有相同的，但未知的赢家-通过研究游戏组成的部分求解器既不能解决也不能简化。我们通过实验验证了这种数据驱动的改进方法可以产生多项式时间部分求解器，可以解决结构化游戏的所有标准基准。对于这些多项式时间部分求解器中的一个，我们甚至无法找到它无法完全解决的唯一随机游戏，尽管我们为此生成了数十亿个不同配置的随机游戏。然而，这里提出的工作还没有任何更深层次的特征，游戏完全解决了这样的部分求解器。
Partial methods play an important role in formal methods and beyond. Recently such methods were developed for parity games, where polynomial-time partial solvers decide the winners of a subset of nodes. We investigate here how effective polynomial-time partial solvers can be in principle by studying polynomial-time interactions of partial solvers. Concretely, we propose simple, generic composition patterns for partial solvers that preserve polynomial-time computability. We show that an implementation of this semantic framework manually discovers new partial solvers – including those that merge node sets that have the same but unknown winner – by studying games that composed partial solvers can neither solve nor simplify. We experimentally validate that this data-driven approach to refinement leads to polynomial-time partial solvers that can solve all standard benchmarks of structured games. For one of these polynomial-time partial solvers, we were unable to find even a sole random game that it won’t solve completely, although we generated a few billion random games of varying configurations to that end. However, the work presented here does not yet offer any deeper characterisations of which games are completely solved by such partial solvers.
平价游戏的拉宾指数：其复杂性和近似值
影响因子：
1
作者：
Huth M
通讯作者：
Huth M