| 一种基于自动机理论的LTL检验符号优化方法 |
| |
| 引用本文： | 钱俊彦,赵岭忠,古天龙.一种基于自动机理论的LTL检验符号优化方法[J].计算机工程,2005,31(23):20-21,27. |
| |
| 作者姓名： | 钱俊彦 赵岭忠 古天龙 |
| |
| 作者单位： | 桂林电子工业学院计算机系,桂林,541004 |
| |
| 基金项目： | 国家“十五”国防预研基金资助项目，广西自然科学基金资助项目(0141046) |
| |
| 摘 要： | 模型检验是一种重要的形式化自动验证技术。检验一个模型是否满足LTL公式,可以把LTL公式转换为一个表示相同无穷状态序列的ω自动机,通过转换后的ω自动机与系统自动机的乘积判空来进行模型检验。由于自动机的体积是模型检验的一个关键性问题,为了得到尽可能小的自动机,在LTL公式转换为ω自动机之前,对LTL公式进行预处理来减少冗余,然后基于ROBDD,通过布尔技术优化自动机。
|
| 关 键 词： | 线性时态逻辑 ω自动机 Büchi自动机 ROBDD |
| 文章编号： | 1000-3428（2005）23-0020-02 |
| 修稿时间： | 2004年10月12 |
A Symbolic Optimization Method for Model Checking of LTL Based on Automaton Theory |
| |
| QIAN Junyan,ZHAO Lingzhong,GU Tianlong.A Symbolic Optimization Method for Model Checking of LTL Based on Automaton Theory[J].Computer Engineering,2005,31(23):20-21,27. |
| |
| Authors: | QIAN Junyan ZHAO Lingzhong GU Tianlong |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
