基于启发式SCCs的广义Büchi自动机判空检测算法

• 作者: 徐中伟 王曦
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 模型检测 Büchi自动机 on-the-fly算法 判空检测
• 年，卷（期）: 2012,（1）
• 所属期刊栏目: 学术论文
• 页码范围: 95-102
• 分类号: TP301
• 字数: 7394字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2012.01.016

摘要

基于自动机理论模型检测的一个关键算法是判断有穷状态系统是否满足属性的判空检测.对标准Büchi自动机作判空检测,容易引起状态爆炸.本文以TGBA为研究对象,提出基于启发式SCCs的广义Büchi自动机判空检测算法.该算法在on-the-fly算法的基础上结合启发式深度优先搜索和SCCs检测算法,能较快地判断TGBA的非空性.通过正确性证明、复杂性分析和实验验证了该算法的正确可行性.在TGBA非空的情况下,该算法的时空性能比已有算法更优.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐中伟	同济大学电子与信息工程学院	95	644	13.0	20.0
2	王曦	同济大学电子与信息工程学院	15	79	6.0	8.0