段珊，王金娟

（湖南涉外经济学院信息科学与工程学部，长沙 410025）

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

段珊，王金娟

（湖南涉外经济学院信息科学与工程学部，长沙 410025）

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

可达状态；固定点；饱和算法；MDDs

0 引言

可达状态空间的计算与存储是形式化验证工具必需面对的关键性问题，例如模型检测器，它需要穷尽系统的所有可达状态来实现系统性质的确认。随着所研究系统的复杂化，如何构建和存储巨大的状态空间是当前数字系统一个瓶颈。以BDD[1]为代表的符号技术使符号模型检测[2]技术在同步系统中运用取得了较大的成功。但在异步系统中，由于事件行为交替执行的不确定性，它依然不得不面临空间状态的爆炸问题。

Ciardo和Andrew在SMART[3]（Stochastic Model checking Analyzer for Reliability and Timing）这个模型检测工具中采用了一种基于MDDs[4]存储结构，利用不动点理论计算可达状态的饱和算法[5-6]。该算法针对分布式异步系统的特性，通过对其高层模型的逻辑结构在MDD结构上的映射关系的定义，采用有效的迭代策略实现了可达状态空间的存储与建立。……