论文标题
使用决策图紧凑代表状态空间进行显式模型检查
Using Decision Diagrams to Compactly Represent the State Space for Explicit Model Checking
论文作者
论文摘要
在显式模型检查过程中可到达的大量状态是可扩展性的主要瓶颈。本文介绍了使用决策图以紧凑而有效表示非常大的状态空间的方法。异步系统是可能的，因为通过过渡连接的两个系统状态通常具有许多相同的局部部分。使用决策图可以通过不使用内存在不同状态之间存储冗余信息来大大减少内存需求。本文考虑了为此目的的多价值决策图。此外，还描述了一种减少使用这些图表的运行时开销的技术。实验结果和与模型检查器旋转中实现的状态压缩方法的比较表明，本文中介绍的方法可有效地存储具有可接受的运行时开销的较大状态空间。
The enormous number of states reachable during explicit model checking is the main bottleneck for scalability. This paper presents approaches of using decision diagrams to represent very large state space compactly and efficiently. This is possible for asynchronous systems as two system states connected by a transition often share many same local portions. Using decision diagrams can significantly reduce memory demand by not using memory to store the redundant information among different states. This paper considers multi-value decision diagrams for this purpose. Additionally, a technique to reduce the runtime overhead of using these diagrams is also described. Experimental results and comparison with the state compression method as implemented in the model checker SPIN show that the approaches presented in this paper are memory efficient for storing large state space with acceptable runtime overhead.
