用决策图表示显式模型检验的状态空间
Using Decision Diagrams to Compactly Represent the State Space for Explicit Model Checking
摘要：
在显式模型检验过程中可达到的大量状态是可伸缩性的主要瓶颈。本文提出了一种用决策图表示大型状态空间的方法。这对于异步系统是可能的，因为通过转换连接的两个系统状态通常共享许多相同的局部部分。使用决策图可以通过不使用存储器来存储不同状态之间的冗余信息来显著减少存储器需求。本文认为多值决策图为此目的。此外，还描述了减少使用这些图的运行时开销的技术。实验结果和比较的状态压缩方法中实现的模型检查SPIN表明，本文提出的方法是内存有效的存储大的状态空间与可接受的运行时开销。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
