| 基于自动机理论的符号模型检验 |
| |
| 引用本文： | 钱俊彦,赵岭忠.基于自动机理论的符号模型检验[J].兰州理工大学学报,2008,34(5). |
| |
| 作者姓名： | 钱俊彦 赵岭忠 |
| |
| 作者单位： | 桂林电子科技大学,计算机与控制学院,广西,桂林,541004 |
| |
| 基金项目： | 国家自然科学基金，国家自然科学基金，广西自然科学基金 |
| |
| 摘 要： | 状态爆炸是模型检验需解决的一个关键问题.基于GPVW算法,以及从LTL公式导出识别该公式的Büchi自动机,用OBDD符号表示,通过符号操作求解自动机乘积.采用符号方法求解出含有初始状态或接受状态的最大连通图,判断自动机是否存在初始状态能否到达含有接收状态的最大连通分支,从而判定所接受的语言是否非空来模型检验LTL公式.采用本文所提出模型检验LTL公式的方法,能在一定程度上解决空间爆炸问题.
|
| 关 键 词： | Büchi自动机 |
Symbolic model checking based on automat theory |
| |
| QIAN Jun-yan,ZHAO Ling-zhong.Symbolic model checking based on automat theory[J].Journal of Lanzhou University of Technology,2008,34(5). |
| |
| Authors: | QIAN Jun-yan ZHAO Ling-zhong |
| |
| Institution: | QIAN Jun-yan,ZHAO Ling-zhong (Computer Department,Guilin University of Electronic Technology,Guilin 541004,China) |
| |
| Abstract: | |
| |
| Keywords: | LTL OBDD |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
