A Symbolic Algorithm for Shortest EG Witness Generation
A Symbolic Algorithm for Shortest EG Witness Generation
复制标题
最短EG见证生成的符号算法
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Gianfranco Ciardo
中科院分区：
文献类型：
--
作者：
Yang Zhao;Xiaoqing Jin;Gianfranco Ciardo
见证生成是模型检查器的基本功能，但为 EG CTL 公式生成最短见证长期以来一直是理论和实践相关的难题。我们提出了一种基于边缘值多路决策图的最短 EG 见证生成的符号方法。我们采用不动点符号迭代来计算距离信息增强的传递闭包，并使用饱和算法来应对这种方法的高计算复杂度。我们还将这种方法扩展到解决其他财产的最短证人生成和最短公平证人生成问题。实验结果表明，我们的方法可以生成最短的见证，而使用以前的算法无法在可接受的时间内找到该见证。
Witness generation is a fundamental model checker feature, but generating shortest witnesses for an EG CTL formula has long been a difficult problem of both theoretical and practical relevance. We propose a symbolic approach to shortest EG witness generation based on edge-valued multi-way decision diagrams. We employ a fix point symbolic iteration to compute the transitive closure enhanced with distance information, using the saturation algorithm to cope with the high computational complexity of this approach. We also extend this approach to tackling the shortest witness generation for other properties and the shortest fair witness generation. Experimental results show that our approach can generate a shortest witness which could not be found within acceptable time using previous algorithms.