Practical synthesis of reactive systems from LTL specifications via parity games
Practical synthesis of reactive systems from LTL specifications via parity games
复制标题
DOI：
10.1007/s00236-019-00349-3
复制
发表时间：
2019-03
期刊：
影响因子：
0.6
通讯作者：
Michael Luttenberger;Philipp J. Meyer;Salomon Sickert
中科院分区：
文献类型：
--
作者：
Michael Luttenberger;Philipp J. Meyer;Salomon Sickert
从线性时序逻辑（LTL）规范综合反应式系统是可靠的软件和硬件设计中的一个重要方面。我们提出了经典自动机理论方法对LTL合成的适应性，该方法在工具Strix中实现，该工具赢得了最后两次合成竞赛（Syntcomp 2018/2019）。所提出的方法是（1）结构化的，这意味着在构造中使用的状态具有以多种方式利用的语义结构，它执行（2）向前探索，使得它通常只构造可达状态的一个小子集，并且它是（3）增量的，在这个意义上，它重用来自先前不确定的解决方案尝试的结果。此外，我们提出并研究了不同的指导策略，确定在哪里扩展按需构建的竞技场。此外，我们展示了几种技术提取的实现（Mealy机或电路）从证人的树自动机空检查。最后，所选择的构造使用转换函数的符号表示来减少运行时和内存消耗。我们在Syntcomp 2019基准测试集上评估了所提出的技术，并更详细地展示了所提出的技术与其他领先的LTL合成工具中实现的技术的比较。
The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented in the toolStrixwhich has won the two last synthesis competitions (Syntcomp2018/2019). The presented approach is (1)structured, meaning that the states used in the construction have a semantic structure that is exploited in several ways, it performs a (2)forward explorationsuch that it often constructs only a small subset of the reachable states, and it is (3)incrementalin the sense that it reuses results from previous inconclusive solution attempts. Further, we present and study different guiding heuristics that determine where to expand the on-demand constructed arena. Moreover, we show several techniques for extracting an implementation (Mealy machine or circuit) from the witness of the tree-automaton emptiness check. Lastly, the chosen constructions use a symbolic representation of the transition functions to reduce runtime and memory consumption. We evaluate the proposed techniques on theSyntcomp2019benchmark set and show in more detail how the proposed techniques compare to the techniques implemented in other leading LTL synthesis tools.