摘要
以固定点为数学基础,多值决策图(Multi-Valued Decision Diagrams,MDDs)为存储结构来实现系统可达状态空间建立的饱和算法在异步系统的模型中显示其良好的空间和时间效应。对该算法的理论和实现方法进行详细的阐述和分析,提出通过对当前事件中的扩展链的预先判断,修改原饱和算法来实现取消无扩展链的事件的函数递归调用、新节点的内存空间的申请与回收,达到提高算法的时间和空间效率;并从理论推理和实验上进行验证。
On the mathematical basis of fixed point, MDDs are good for storage structure to realize the computation of reachable state space; the sat- uration algorithm shows its good in space and time effect in asynchronous system. Presents the theory and implementation method of the algorithm in detail and analysis, and puts forward a method that prejudge extension chain of the current event, modifies the original satu- rate event to call for recursive function to realize the expansion of the lower nodes and saturation algorithm to cancel the calling for func- tion, applying and recycle of new node for memory without extension chain, so as to improve the efficiency of the algorithm of time and space. The new method is proved from the theoretical analysis and experiment.
关键词
可达状态
固定点
饱和算法
MDDs
Reachable State Space
Fixed Point
Saturation Algorithm
MDDs
