广义Rabin（1）合成
Generalised Rabin(1) synthesis
摘要：
我们提出了一种新的方法，用于有限状态系统的合成，这是广义反应性（1）合成方法的推广由Piterman，Pnueli和Sa'ar。特别是，我们描述了一种有效的方法来合成系统的线性时间时序逻辑规范，所有的假设和保证有一个拉宾指数为1。我们将展示如何建立一个奇偶校验游戏，最多五种颜色，捕捉所有的解决方案，从这样的规范的合成问题。这个奇偶性博弈有一个适合于符号实现的结构。我们还证明了所得结果在某种意义上是紧的，即，除非P=NP，否则不存在类似的合成方法用于更高Rabin指数的假设和规范。
英文摘要：
We present a novel method for the synthesis of finite state systems that is a generalisation of the generalised reactivity(1) synthesis approach by Piterman, Pnueli and Sa'ar. In particular, we describe an efficient method to synthesize systems from linear-time temporal logic specifications for which all assumptions and guarantees have a Rabin index of one. We show how to build a parity game with at most five colours that captures all solutions to the synthesis problem from such a specification. This parity game has a structure that is amenable to symbolic implementations. We furthermore show that the results obtained are in some sense tight, i.e., that there does not exist a similar synthesis method for assumptions and specifications of higher Rabin index, unless P=NP.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
