一种基于自动机理论的LTL检验符号优化方法

• 作者: 古天龙 赵岭忠 钱俊彦
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 线性时态逻辑 ω自动机 Büchi自动机 ROBDD
• 年，卷（期）: 2005,（23）
• 所属期刊栏目: 博士论文
• 页码范围: 20-21,27
• 页数: 3页
• 分类号: TP301.1
• 字数: 1867字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2005.23.008

摘要

模型检验是一种重要的形式化自动验证技术.检验一个模型是否满足LTL公式,可以把LTL公式转换为一个表示相同无穷状态序列的ω自动机,通过转换后的ω自动机与系统自动机的乘积判空来进行模型检验.由于自动机的体积是模型检验的一个关键性问题,为了得到尽可能小的自动机,在LTL公式转换为ω自动机之前,对LTL公式进行预处理来减少冗余,然后基于ROBDD,通过布尔技术优化自动机.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	古天龙	桂林电子工业学院计算机系	207	1546	18.0	30.0
2	钱俊彦	桂林电子工业学院计算机系	86	238	9.0	10.0
3	赵岭忠	桂林电子工业学院计算机系	64	229	8.0	11.0