Towards Efficient Implementation of Realizability Checking for Reactive System Specifications
Towards Efficient Implementation of Realizability Checking for Reactive System Specifications
复制标题
高效实施反应式系统规范的可实现性检查
DOI：
10.1145/3316615.3316634
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Shigeki Hagihara and Naoki Yonezaki
中科院分区：
文献类型：
--
作者：
Masaya Shimakawa;Atsushi Ueno;Shohei Mochizuki;Takashi Tomita;Shigeki Hagihara and Naoki Yonezaki
可实现性检查用于检测反应式系统规范中人类难以发现的缺陷。然而，这些检查的计算成本很高。为了解决这个问题，研究人员研究了实施此类检查程序的有效方法。在本文中，我们提出了一种新的可实现性检查的实现方法。虽然之前的许多方法都采用了符号方法，但我们采用部分符号方法，其中部分使用二元决策图（BDD）。我们根据我们的方法开发了一个原型可实现性检查器，并通过实验将其与基于其他实现方法的工具进行了比较。与其他工具相比，我们的原型非常高效。
Realizability checking is used to detect flaws in reactive system specifications that are difficult for humans to find. However, these checks are computationally costly. To address this problem, researchers have studied efficient methods for implementing such checking procedures. In this paper, we propose a new implementation method of realizability checking. While symbolic approaches have been adopted in many previous methods, we take a partially symbolic approach, in which binary decision diagrams (BDDs) are used partially. We developed a prototype realizability checker based on our method, and experimentally compared it to tools based on other implementation methods. Our prototype was efficient in comparison to the other tools.