论文标题
象征性平价游戏求解器，产生获胜策略
Symbolic Parity Game Solvers that Yield Winning Strategies
论文作者
论文摘要
奇偶校验游戏对LTL综合起着重要作用，这是最近在LTL合成上的突破所证明的，LTL合成综合，其中一部分依赖于平等游戏解决方案。如果我们想扩展到较大的系统或规格，那么状态空间爆炸仍然是一个主要问题。为了解决这个问题，我们需要研究诸如BDD之类的符号方法，BDD过去一直成功地解决指数较大的系统。因此，必须使用BDD快速运行的符号奇偶校验游戏解决算法，并且可以产生用于合成LTL合成中控制器的获胜策略。 当前的符号平价游戏解决算法不会产生获胜策略。现在，我们提出了两种符号算法，这些算法基于最近提议的FixPoint算法产生获胜策略。我们实施了算法，并使用从Syntcomp 2020获得的基准进行了经验评估它们。我们的结论是，算法与Zielonka递归算法的象征性实施相比，算法具有竞争力或更快，同时也提供了获胜策略。
Parity games play an important role for LTL synthesis as evidenced by recent breakthroughs on LTL synthesis, which rely in part on parity game solving. Yet state space explosion remains a major issue if we want to scale to larger systems or specifications. In order to combat this problem, we need to investigate symbolic methods such as BDDs, which have been successful in the past to tackle exponentially large systems. It is therefore essential to have symbolic parity game solving algorithms, operating using BDDs, that are fast and that can produce the winning strategies used to synthesize the controller in LTL synthesis. Current symbolic parity game solving algorithms do not yield winning strategies. We now propose two symbolic algorithms that yield winning strategies, based on two recently proposed fixpoint algorithms. We implement the algorithms and empirically evaluate them using benchmarks obtained from SYNTCOMP 2020. Our conclusion is that the algorithms are competitive with or faster than an earlier symbolic implementation of Zielonka's recursive algorithm, while also providing the winning strategies.
