Bounded Synthesis for Streett, Rabin, and \text CTL^*
Bounded Synthesis for Streett, Rabin, and \text CTL^*
复制标题
Streett、Rabin 和 ext CTL^* 的有界综合
DOI：
10.1007/978-3-319-63390-9_18
复制
发表时间：
2017
影响因子：
7.7
通讯作者：
R. Bloem
中科院分区：
文献类型：
--
作者：
A. Khalimov;R. Bloem
基于SMT的有界合成使用SMT求解器通过通过Co-Buchi Automata从LTL属性合成系统。在本文中，我们展示了如何扩展有界合成中使用的排名函数，从而扩展了界定的合成方法，将其扩展到Buchi，Parity，Rabin和StreetT条件。我们表明我们可以通过这种方式处理存在和通用属性，因此，我们可以将有限的合成扩展到\（\ text {ctl}^{*} \）。因此，我们获得了上述接受条件（\ text {ctl}^{*} \）的第一个Safraless合成方法和（连接）的第一个合成工具。
SMT-based bounded synthesis uses an SMT solver to synthesize systems from LTL properties by going through co-Buchi automata. In this paper, we show how to extend the ranking functions used in Bounded Synthesis, and thus the bounded synthesis approach, to Buchi, Parity, Rabin, and Streett conditions. We show that we can handle both existential and universal properties this way, and therefore, that we can extend Bounded Synthesis to \(\text {CTL}^{*}\). Thus, we obtain the first Safraless synthesis approach and the first synthesis tool for (conjunctions of) the acceptance conditions mentioned above, and for \(\text {CTL}^{*}\).