Dynamic state space partitioning for external memory state space exploration

作者：Evangelista Sami^*; Kristensen Lars Michael

来源：Science of Computer Programming, 2013, 78(7): 778-795.

DOI：10.1016/j.scico.2011.09.005

• Model checking
• Explicit state space exploration
• External memory verification
• Distributed verification
• State space partitioning
• State explosion problem

We describe a dynamic partitioning scheme useable by explicit state space exploration techniques that divide the state space into partitions, such as many external memory and distributed model checking algorithms. The goal of the scheme is to reduce the number of transitions that link states belonging to different partitions, and thereby limit the amount of disk access and network communication. We report on several experiments made with our verification platform ASAP that implements the dynamic partitioning scheme proposed in this paper. The experiments demonstrate the importance of exploiting locality to reduce cross transitions and 10 operations, and using informed heuristics when choosing components to be used as a basis for partition refinement. The experiments furthermore show that the proposed approach improves on earlier techniques and significantly outperforms these when provided with access to the same amount of bounded RAM.

• 出版日期2013-7-1