Symbolic State-Space Generation of Asynchronous Systems Using Extensible Decision Diagrams
Symbolic State-Space Generation of Asynchronous Systems Using Extensible Decision Diagrams
复制标题
使用可扩展决策图生成异步系统的符号状态空间
DOI：
10.1007/978-3-540-95891-8_52
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Gianfranco Ciardo
中科院分区：
文献类型：
--
作者：
Min Wan;Gianfranco Ciardo
我们提出了一种新类型的规范决策图，它允许一个更有效的符号状态空间生成一般异步系统，允许在飞行中扩展可能的状态变量域。在我们的工具${\rm S\克恩-.11em\raise.39ex\hbox{\sc m}\克恩-.22em A\克恩-.21em\raise.39ex\hbox {\sc r}\克恩-.16emT}$中使用这种新的数据结构实现了宽度优先和基于饱和度的状态空间生成之后，我们能够展示出相对于传统“静态”决策图的实质性效率改进。由于我们以前的工作表明，饱和度优于宽度优先的方法，这种新结构的饱和度，现在可以说是最先进的异步系统的符号状态空间生成算法。
We propose a new type of canonical decision diagrams, which allows a more efficient symbolic state-space generation for general asynchronous systems by allowing on-the-fly extension of the possible state variable domains. After implementing both breadth-first and saturation-based state-space generation with this new data structure in our tool ${\rm S\kern-.11em\raise.39ex\hbox{\sc m}\kern-.22em A\kern-.21em\raise.39ex\hbox{\sc r}\kern-.16emT}$, we are able to exhibit substantial efficiency improvements with respect to traditional "static" decision diagrams. Since our previous works demonstrated that saturation outperforms breadth-first approaches, saturation with this new structure is now arguably the state-of-the-art algorithm for symbolic state-space generation of asynchronous systems.