一种基于MDDs的可达状态的算法研究

摘要

以固定点为数学基础,多值决策图（Multi-Valued Decision Diagrams,MDDs）为存储结构来实现系统可达状态空间建立的饱和算法在异步系统的模型中显示其良好的空间和时间效应。对该算法的理论和实现方法进行详细的阐述和分析,提出通过对当前事件中的扩展链的预先判断,修改原饱和算法来实现取消无扩展链的事件的函数递归调用、新节点的内存空间的申请与回收,达到提高算法的时间和空间效率;并从理论推理和实验上进行验证。