广义Rabin(1)综合
计算机科学中的逻辑
2015-03-13 v2
摘要
我们提出了一种新颖的有限状态系统综合方法，该方法是Piterman、Pnueli和Sa'ar的广义反应性(1)综合方法的推广。特别地，我们描述了一种高效方法，用于从所有假设和保证的Rabin指数均为1的线性时序逻辑规约综合系统。我们展示了如何构建一个最多包含五种颜色的奇偶博弈，该博弈捕获了从该规约出发的综合问题的所有解。该奇偶博弈的结构适合符号化实现。此外，我们证明了所得结果在某种意义上是紧的，即除非P=NP，否则不存在针对更高Rabin指数的假设和规约的类似综合方法。
引用
@article{arxiv.1003.1684,
title = {Generalised Rabin(1) synthesis},
author = {Ruediger Ehlers},
journal= {arXiv preprint arXiv:1003.1684},
year = {2015}
}
备注
14 pages