| 一种基于编码的OBDD模型检测的算法实现 |
| |
| 引用本文： | 马晓龙,顾滨兵,刘鑫淼. 一种基于编码的OBDD模型检测的算法实现[J]. 舰船电子工程, 2011, 31(10): 118-121 |
| |
| 作者姓名： | 马晓龙 顾滨兵 刘鑫淼 |
| |
| 作者单位： | 91404部队,秦皇岛,066000 |
| |
| 摘 要： | ![]()
文章根据OBDD模型检测的基本思想并结合一个微波炉模型实例来介绍一种基于状态编码的OBDD模型检测算法实现。该算法实现通过介绍自行开发的OBDD模型检测器,具体描述了OBDD的生成、化简以及使用OBDD进行模型检测的具体实现算法以及OBDD模型检测的全过程,该算法实现简洁易读,可以直接应用于相关程序的开发。
|
| 关 键 词： | OBDD 模型检测 状态编码 CTL公式 |
An Algorithm of OBDD Model Checking Based on State Encoding |
| |
| Ma Xiaolong Gu Binbing Liu Xinmiao. An Algorithm of OBDD Model Checking Based on State Encoding[J]. Ship Electronic Engineering, 2011, 31(10): 118-121 |
| |
| Authors: | Ma Xiaolong Gu Binbing Liu Xinmiao |
| |
| Affiliation: | Ma Xiaolong Gu Binbing Liu Xinmiao(No.91404 Troops of PLA,Qinhuangdao 066000) |
| |
| Abstract: | ![]()
|
| |
| Keywords: | OBDD model checking state encoding CTL formula |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
|
