您的位置：首页 > 新闻 > CCF新闻 > 工作委员会 > 计算机术语审定委员会

联手形式化方法专业委员会：“状态空间爆炸”术语发布 | CCF术语快线

阅读量:56 2022-05-06 收藏本文

本期发布术语热词：状态空间爆炸(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.

[14]C. Courcoubetis, M.Y. Vardi, P. Wolper, et al., “Memory efficient algorithms for verification of temporal properties,” Formal Methods in System Design, vol. 1, pp. 275-288, 1992.

[15]R. Mateescu and J.I. Requeno, “On-the-fly model checking for extended action-based probabilistic operators,” International Journal on Software Tools for Technology Transfer, vol. 20, no. 5, pp. 563-587, 2018.

[16]F. B?nneland et al., “Simplification of CTL formulae for efficient model checking of Petri nets,” in Proc. Int. Conf. Appl. Theory Petri Nets Concurrency, 2018, pp. 143–163.

[17]N. Rezaee and H. Momeni, “A hybrid meta-heuristic approach to cope with state space explosion in model checking technique for deadlock freeness,” J. AI Data Mining, vol. 8, no. 2, pp. 189-199, 2020.

[18]L. F. He, G. J. Liu, and M. C. Zhou, “Petri-net-based model checking for privacy-critical multiagent systems,” IEEE Trans. Comput. Social Syst., 2022.

[19]M. Osama and A. Wijs., “GPU acceleration of bounded model checking with ParaFROST,” in Proc. Int. Conf. Comput. Aided Ver., 2021, pp. 447-460.

[20]M. N. Aung, Y. Phyo, C. M. Do, et al., “A divide and conquer approach to eventual model checking,” Mathematics, vol. 9, no. 368, pp. 1-16, 2021.

[21]M. Yasrebi, V. Rafe, and S. Nejatian, “An efficient approach to state space management in model checking of complex software systems using machine learning techniques,” J. Int. & Fuzzy Syst., vol. 38, no. 2, pp. 1761-1773, 2020.

作者介绍

术语工委及术语平台介绍：

计算机术语审定委员会(Committee on Terminology)主要职能为收集、翻译、释义、审定和推荐计算机新词，并在CCF平台上宣传推广。这对厘清学科体系，开展科学研究，并将科学和知识在全社会广泛传播，都具有十分重要的意义。

术语众包平台CCFpedia的建设和持续优化，可以有效推进中国计算机术语的收集、审定、规范和传播工作，同时又能起到各领域规范化标准定制的推广作用。

新版的CCFpedia计算机术语平台(http://term.ccf.org.cn)将术语的编辑运营与浏览使用进行了整合，摒弃老版中跨平台操作的繁琐步骤，在界面可观性上进行了升级，让用户能够简单方便地查阅术语信息。同时，新版平台中引入188体育app官网：的方式对所有术语数据进行组织，通过图谱多层关联的形式升级了术语浏览的应用形态。