| 《计算机学报》文章摘要 全文下载 | |
| 文章题目 | 基于SCC空性检测中状态空间的缩减方法 |
| 作者 | 晏荣杰1),2) 张文亮1),2) 唐稚松1) |
| 作者单位 | (中国科学院软件研究所计算机科学国家重点实验室 北京 100190) (中国科学院研究生院 北京 100039) |
| 发表年份 | 2008 |
| 发表月份 | 6期(979—988) |
| 文章摘要 | 摘要 对Couvreur提出的基于强连通图的空性检测算法进行改进， 使基于嵌套的深度优先搜索与基于强连通图搜索算法的优势结合起来， 在对基于迁移的扩展(具有多个可接受条件)Büchi自动机进行空性检测过程中， 使用一个布尔变量标识一个状态， 不仅节省了内存消耗，而且一般情况下的性能明显优于已有的算法， 最坏情况等同于Couvreur的算法.同时反例寻找过程等同于基于强连通图的检测算法. 关键词：空性检测；基于迁移的扩展Büchi自动机；可接受条件 |