一种基于Büchi自动机的LTL程序模型检测方法

• 作者: 罗清胜
• 来源期刊: 计算机与现代化
• 学科: 工学
• 关键词: 线性时序逻辑 Büchi自动机 模型检测
• 年，卷（期）: 2010,（8）
• 页码范围: 58-61
• 分类号: TP18
• 字数: 3630字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-2475.2010.08.017

摘要

时序逻辑程序的形式化验证对提高程序的正确性具有重要意义.基于自动机的理论,用标签转移系统(S)表示程序的行为,用时序逻辑公式(F)描述程序的性质,构建相应的Büchi自动机,从而证明形式化公式SF是否可满足.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	罗清胜	江西财经大学国际学院	3	5	1.0	2.0