简洁系统的合成
摘要：从规范中合成适当的系统最近引起了很多关注。理论结果表明，这个问题是非常复杂的，例如，对于LTL规范，合成系统的复杂度是2EXPTIME完全的，对于CTL规范，复杂度是EXPTIME完全的。然而，反对意见是时态规范非常紧凑，复杂度反映的是构建的系统的规模。在这方面，复杂度也许应该相对于最小满足系统的规模来指定。仔细观察可以发现，系统的规模在这些论点中被表示为其状态空间的大小。这种观点有些不同寻常，因为状态空间可以比合理实现（如电路或程序）的大小大指数倍。尽管这种替代性的系统规模度量更加直观（例如，这是模型检查问题的标准度量方式），但合成研究目前仍以显式状态空间为度量方式。这引发了一个问题，即是否总是存在一个小的系统。在本文中，我们证明了当且仅当PSPACE = EXPTIME时才存在这种情况。
作者：John Fearnley, Doron Peled, Sven Schewe
论文ID：1202.5449
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2012-05-07