简洁系统的综合
Synthesis of Succinct Systems
摘要：
最近，从规范中合成正确的设计系统引起了人们的广泛关注。理论结果表明，这个问题是非常棘手的，例如，对于LTL规范，系统的合成是2 EXPTIME-完全的;对于CTL规范，系统的合成是EXPTIME-完全的。然而，反对它的一个论点是，时间规格是高度紧凑的，复杂性反映了大规模的系统构造。在这方面，复杂性也许应该相对于最小满意系统的大小来指定。仔细观察就会发现，系统的大小是以状态空间的大小等参数来表示的。这种观点有点不标准，因为状态空间可以指数地大于合理实现（如电路或程序）的大小。虽然合成系统的大小的这种可选测量更直观（例如，这是测量模型检验问题的标准方式），迄今为止，关于综合的研究停留在根据显式状态空间来测量系统。这就提出了一个问题，即是否总是存在一个小系统。在本文中，我们证明了这种情况，当且仅当，PSPACE = EXPTIME。
英文摘要：
Synthesis of correct by design systems from specification has recently attracted much attention. The theoretical results imply that this problem is highly intractable, e.g., synthesizing a system is 2EXPTIME-complete for an LTL specification, and EXPTIME-complete for a CTL specification. However, an argument against it is that the temporal specification is highly compact, and the complexity reflects the large size of the system constructed. In that respect, the complexity should, perhaps, be specified relative to the size of the minimal satisfying system. A careful observation reveals that the size of the system is presented in such arguments as the size of its state space. This view is a bit nonstandard, in the sense that the state space can be exponentially larger than the size of a reasonable implementation such as a circuit or a program. Although this alternative measure of the size of the synthesized system is more intuitive (e.g., this is the standard way model checking problems are measured), research on synthesis has so far stayed with measuring the system in terms of the explicit state space. This raises the question of whether or not there always exists a small system. In this paper, we show that this is the case if, and only if, PSPACE = EXPTIME.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
