一种基于编码的OBDD模型检测的算法实现

• 作者: 刘鑫淼 顾滨兵 马晓龙
• 来源期刊: 舰船电子工程
• 学科: 工学
• 关键词: OBDD 模型检测 状态编码 CTL公式
• 年，卷（期）: 2011,（10）
• 所属期刊栏目: 计算机与网络安全
• 页码范围: 118-121
• 分类号: TP312
• 字数: 2942字
• 语种: 中文
• DOI: 10.3969/j.issn.1627-9730.2011.10.034

摘要

文章根据OBDD模型检测的基本思想并结合一个微波炉模型实例来介绍一种基于状态编码的OBDD模型检测算法实现。该算法实现通过介绍自行开发的OBDD模型检测器,具体描述了OBDD的生成、化简以及使用OBDD进行模型检测的具体实现算法以及OBDD模型检测的全过程,该算法实现简洁易读,可以直接应用于相关程序的开发。