本期发布术语热词：状态空间爆炸(State space explosion)。
状态空间爆炸(State space explosion)
作者：刘关俊（同济大学），何雷锋（同济大学）
InfoBox：
中文名：状态空间爆炸（模型检测）
外文名：State space explosion
学科：计算机科学技术
实质：模型检测时生成的状态数目呈指数级增长，远远超过了计算机的内存存储能力与搜索能力。
基本简介：
模型检测[1,2]是一种验证系统（特别是并发系统）是否满足规范的形式化方法，基本策略是通过遍历系统状态空间来完成系统验证。然而，系统状态的数目随着系统规模的增加—特别是并发分量的增加—而呈指数级增长，这就是状态空间爆炸问题，是模型检测面对的挑战之一[1,2]。
解决状态空间爆炸问题的经典方法，是基于有序二叉决策图 (OBDD) 的状态压缩法[3,4,5,6]；一个状态集合通过一个OBDD来表示，而不需一一列举集合中的元素；这种方法可以指数级缩小状态集合所占用的存储空间，而基于OBDD的模型检测可通过不动点算法实现。另一种较有效的方法是偏序约简[7,8,9,10]，适用于解决异步并发模型交替执行导致的状态空间爆炸；它利用事件的相互独立性减少验证路径，从而缩小所产生的状态空间。抽象技术[11]也是一种重要的途径，在验证系统是否满足某个给定规范时，简化一些细节，删除与该规范无关的构件并保留相关部分，从而构建抽象系统，进而对该抽象系统进行分析，使得状态空间大大减少。还有一种较实用的方法，是有界模型检测[12,13]：给定一个界值k，把验证系统是否在k步运行内满足规范的问题转化为命题公式是否可满足的问题（通常，公式用来表达所期望的设计规范的反面），而命题公式的可满足性可通过布尔可满足性求解器求解；公式可满足则说明存在一个长度为k的路径不满足规范，公式不可满足则说明系统在k步内是安全的，此时增大k的值重复以上过程直到找到一个有限路径不满足规范为止，当k的值达到系统的循环直径时仍然找不到一个这样的路径则停止循环，此时说明系统满足规范；有界模型检测通常可以快速找到反例（如果系统存在反例），且保证找到的反例是长度最短、最简洁的。运行时(On-the-Fly)模型检测[14,15]，也是缓解状态空间爆炸的一种策略，不需事先生成完整的状态集，而是在验证给定规范的过程中，动态生成所需部分，从而节约内存开销。另外一些方法，适用于一些具体的应用场景，例如，通过简化时序逻辑公式以减少对状态空间的遍历次数[16]，从而一定程度上缓解状态空间爆炸问题；又如，利用人工蜂群算法和模拟退火算法，只需遍历部分状态空间即可检测整个系统是否存在死锁[17]。状态空间爆炸通常是并发系统固有的现象，也说明并发系统的设计与分析验证并非易事。现有方法在一定程度上缓解了状态空间爆炸导致的系统正确性难以验证的问题，但仍有很多值得研究的方面。例如，一个OBDD的规模依赖于变量序，不恰当的变量序同样可以造成OBDD结点数呈指数级增长，因此，如何构造一个恰当的变量序是一个值得研究的问题[18]。又如，在有界模型检测中，如何利用多核和GPU辅助以加快可满足性求解器的求解速度同样是一个很好的研究点[19]。现实中通常会把一个很难解决的大问题分解为多个较容易解决的小问题，这种分而治之的思想同样可以用于模型检测[20]，这对于缓解状态空间爆炸提供了一种新思路。此外，模型检测与机器学习相结合以避免遍历状态空间[21]，是一个新的研究方向，如何利用机器学习技术预测命题公式满足与否、以及如何在提高效率的同时保证足够的准确率，都值得探索。
参考文献
[1]E. M. Clarke and E. A. Emerson, “Design and synthesis of synchronization skeletons using branching time temporal logic,” in Proc. Workshop Logic Program, 1981, pp. 52-71.
[2]J. P. Queille and J. Sifakis, “Specification and verification of concurrent systems in CESAR,” in Proc. Int. Symp. Programming, 1982, pp. 337-351.[3]R. E. Bryant, “Graph-based algorithms for Boolean function manipulation,” IEEE Trans. Comput., vol. C-35, no. 8, pp. 677-691, 1986.[4]J. R. Burch, E. M. Clarke, K. L. McMillan, et al., “Symbolic model checking: 1020 states and beyond,” Inf. Comput., vol. 98, no. 2, pp. 142-170, 1992.[5]L. F. He and G. J. Liu, “Petri net based CTL model checking: Using a new method to construct OBDD variable order,” in Proc. Int. Symp. Theor. Aspects Softw. Eng., 2021, pp. 159-166.[6]古天龙，徐周波，有序二叉决策图及应用，科学出版社，2009. [7]P. Godefroid, J. van Leeuwen, J. Hartmanis, et al., Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. Heidelberg: Springer, 1996.[8]E. M. Clarke, O. Grumberg, M. Minea, and D. Peled, “State space reduction using partial order techniques,” Int. J. Softw. Tools Technol. Transf. (STTT), vol. 2, no. 3, pp. 279-287, 1999.[9]J. Esparza and K. Heljanko, Unfoldings: a partial-order approach to model checking. Springer Science & Business Media, 2008.[10]刘关俊，Petri网的元展: 一种并发系统模型检测方法，科学出版社，2020.[11]E. M. Clarke, O. Grumberg, S. Jha, et al., “Counterexample-guided abstraction refinement for symbolic model checking,” J. ACM (JACM), vol. 50, no. 5, pp. 752-794, 2003.[12]N. Amla, R. Kurshan, K. L. McMillan, et al., “Experimental analysis of different techniques for bounded model checking,” in Proc. Int. Conf. Tools Alg. Const. Analy. Syst., 2003, pp. 34-48.[13]E. M. Clarke, W. Klieber, M. Nová?ek, et al., “Model checking and the state explosion problem,” LASER Summer School Soft. Eng., 2011, pp. 1-30.
返回首页
