Interval diagram techniques for symbolic model checking of Petri nets
Interval diagram techniques for symbolic model checking of Petri nets
复制标题
Petri网符号模型检验的区间图技术
DOI：
10.1145/307418.307452
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
L. Thiele
中科院分区：
文献类型：
--
作者：
Karsten Strehl;L. Thiele
符号模型检验试图通过隐式构造状态空间来减少状态爆炸问题。主要的限制因素是符号表示的大小，这些符号表示大多存储在巨大的二元决策图中。本文提出了一种新的Petri网及相关计算模型的符号模型检验方法，它克服了传统方法的某些缺点，并取得了较好的效果。我们的方法是基于一种新的，高效的形式表示的多值函数称为区间决策图（IDD）和相应的图像计算技术，使用区间映射图（IMD）。介绍了IDD和IMD，描述了它们的特性，并用实验结果说明了新方法的可行性。
Symbolic model checking tries to reduce the state explosion problem by implicit construction of the state space. The major limiting factor is the size of the symbolic representation mostly stored in huge binary decision diagrams. A new approach to symbolic model checking of Petri nets and related models of computation is presented, outperforming the conventional one and avoiding some of its drawbacks. Our approach is based on a novel, efficient form of representation for multi-valued functions called interval decision diagram (IDD) and the corresponding image computation technique using interval mapping diagrams (IMDs). IDDs and IMDs are introduced, their properties are described, and the feasibility of the new approach is shown with some experimental results.