模型检测中状态爆炸及其优化策略研究

摘要：

模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,简洁明了和自动化程度高,在生产实践中得到了广泛的应用,其主要缺陷是状态爆炸问题。阐述了模型检测的基本思想和相关理论,给出一些处理状态爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单对模型检测新进展的研究热点和现状进行了分析和介绍。

关键词： 模型检测 状态爆炸 形式验证 时态逻辑 优化策略 有限状态系统

作者: 王飞明 胡元闯 董荣胜

作者单位: 桂林电子科技大学 计算机系 广西 桂林 541004 桂林电子科技大学 计算机系 广西 桂林541004

会议类型: 国内会议

会议名称: 广西计算机学会2008年年会

会议地点: 广西北海

会议语种:中文

页码: 105-111

在线出版日期: 2008-09-01（万方平台首次上网日期，不代表论文的发表时间）