线性时态逻辑可满足工具的设计与实现

发布时间：2023-02-20 20:53

　　线性时态逻辑(LTL)自从上个世纪七十年代被引入计算机科学领域之后,得到了很大的发展。现如今,LTL作为一种形式化的性质规范描述,已在程序验证与分析、程序综合、数据库和人工智能领域被广泛使用。对于逻辑语言LTL来讲,可满足性问题是一个亟待解决的关键性问题。与此同时,对于工业界而言,该问题也是十分重要的。因为对于程序验证、综合或是人工智能领域而言,不可满足的公式是没有意义的。本文就LTL的可满足性问题展开,介绍了一种新的算法OFOA(第三章)。传统方法中,对LTL的可满足性性判定需要先将其转化为等价的Buchi自动机,然后再进行判断；而我们的算法提供了一套全新的推理框架,可以在公式展开的同时对其可满足性进行判断,这就是一个明显的优化。按照"on the fly"的思想,我们为LTL公式定义了“义务集合”的概念,从而极大加速了公式可满足性的判定过程。以该算法为基础,我们设计实现了LTL可满足性判定工具Aalta,文章的后半部分主要介绍该工具的设计框架、相应的数据结构和核心算法。为了验证算法的效率,我们选取目前公认的最出色的可满足性检查工具(PANDA、Cadence SMV和SPOT)进行...

【文章页数】：63 页

【学位级别】：硕士

【文章目录】：
摘要
ABSTRACT
第一章：绪论
    1.1 线性时态逻辑的发展历程
    1.2 线性时态逻辑的应用场景
        1.2.1 程序验证
        1.2.2 程序综合
    1.3 线性时态逻辑的研究现状
    1.4 本文的选题与主要工作
第二章 背景知识
    2.1 LTL线性时态逻辑
        2.1.1 LTL语法
        2.1.2 LTL语义
    2.2 Büchi自动机
    2.3 迁移系统
    2.4 LTL可满足性检查算法
        2.4.1 基于tableau方法的LTL可满足性检查
        2.4.2 转化为模型检查问题的LTL可满足性检查
    2.5 本章小结
第三章 LTL可满足性算法框架设计
    3.1 从LTL到Buchi自动机
    3.2 义务加速检查
    3.3 基于义务集合的可满足性检查
    3.4 基于SAT技术的LTL可满足性检查
    3.5 本章小结
第四章 LTL可满足性工具详细设计与实现
    4.1 数据结构
        4.1.1 公式结构
        4.1.2 DNF结构
        4.1.3 存储结构
    4.2 核心算法
        4.2.1 规范化
        4.2.2 化简
        4.2.3 一致性判断
        4.2.4 寻找强连通分量
    4.3 Aalta的实现
        4.3.1 输入
        4.3.2 输出
        4.3.3 语法解析器
        4.3.4 公式构建器
        4.3.5 可满足性检查器
    4.4 本章小结
第五章 实验结果
    5.1 实验工具
    5.2 实验平台
    5.3 实验输入
    5.4 实验结果
    5.5 本章小结
第六章 总结与展望
参考文献
硕士阶段发表论文和科研情况
致谢



本文编号：3747296