|
|||||
|
|
| 基于惰性切片的线性时态逻辑性质验证 | |
| 引用本文： | 黄宏涛,王静,叶海智,黄少滨.基于惰性切片的线性时态逻辑性质验证[J].吉林大学学报(工学版),2015,45(1). |
| 作者姓名： | 黄宏涛 王静 叶海智 黄少滨 |
| 作者单位： | 1. 河南师范大学河南省教育信息工程技术研究中心,河南新乡,453007 2. 中国石化管道储运公司新乡输油处信息中心,河南新乡,453007 3. 哈尔滨工程大学计算机科学与技术学院,哈尔滨,150001 |
| 摘 要： | 惰性切片是一种有效的状态空间缩减方法,但是它无法直接判定一个模型是否满足所期望的线性时间性质。针对该问题,提出了一种基于惰性切片的线性时态逻辑公式验证方法。该方法首先构造给定线性时态逻辑公式的否定Büchi自动机与系统模型的乘积自动机,然后使用惰性切片算法在该乘积自动机上以惰性方式搜索可接受迹,从而把线性时间性质验证问题转换为通过可达性分析搜索可接受状态的不变性检测过程。实验结果证明,基于惰性切片的线性时态逻辑公式验证算法在不损失验证结果正确性的前提下使惰性切片算法具备了验证线性时间性质的能力,同时也有效提高了LTL模型检测方法的可扩展性。 |
| 关 键 词： | 计算机软件 模型检测 惰性切片 线性时态逻辑 Büchi自动机 乘积自动机 |
Lazy slicing based method for verifying linear temporal logic property |
|
| HUANG Hong-tao,WANG Jing,YE Hai-zhi,HUANG Shao-bin.Lazy slicing based method for verifying linear temporal logic property[J].Journal of Jilin University:Eng and Technol Ed,2015,45(1). | |
| Authors: | HUANG Hong-tao WANG Jing YE Hai-zhi HUANG Shao-bin |
| Abstract: | |
| Keywords: | computer software model checking lazy slicing linear temporal logic Büchi automata product automata |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |