线性时态逻辑中若干基础问题的研究

发布时间：2024-02-19 17:18

　　线性时态逻辑(LTL)现今已被广泛运用于计算机科学领域(CS)。它常作为描述系统行为的性质语言,用在程序验证、程序综合与人工智能(AI)等研究方向。比方说,为了验证给定的系统是否满足其对应的性质规范(通常是用LTL来书写的),模型检测技术会将该性质的否定转成与其等价的Buchi自动机,把它与系统模型求交得到新的自动机,并在这新的自动机上检查其接收的语言是否为空,从而可以判定系统是否满足该性质。从LTL在CS中的应用场景我们可以抽取出LTL的两个基本研究问题：一是从LTL公式到与其等价的Buchi自动机的转换算法,这个算法要被频繁的应用于程序验证、程序综合等方向；还有一个就是LTL公式的可满足性检查问题-这是因为在实际的应用场景中不可满足的公式是没有意义的。本文因此就以上两个问题展开,提出一些新的算法与解决方案。 我们首先探索从LTL公式到其等价的Buchi自动机的转换问题,并提出一种新的转换算法(第三章)。和其他方法相比,我们的方案避免了中间自动机的生成,这就潜在的可以加快构造的进程。我们实现了该算法并与SPOT工具作了比较-SPOT是目前为止公认度较高的最好的LTL到Buchi自动机...

【文章页数】：137 页

【学位级别】：博士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 线性时态逻辑在计算机领域的重要性
    1.2 线性时态逻辑在若干问题中的研究现状
    1.3 本文的选题与主要工作
第二章 基础知识
    2.1 LTL线性时态逻辑
    2.2 Buchi自动机
    2.3 LTL_f有限线性时态逻辑
第三章 从LTL到Buchi自动机的转化
    3.1 背景介绍
    3.2 一个驱动例子
    3.3 LTL迁移系统
    3.4 转换算法
    3.5 实验仿真
    3.6 本章小结
第四章 LTL可满足性检查
    4.1 背景介绍
    4.2 义务加速检查
    4.3 基于义务集的完备的可满足性检查
    4.4 中心定理的证明
    4.5 实验仿真
    4.6 本章小结
第五章 基于SAT技术的LTL可满足性检查
    5.1 背景介绍
    5.2 应用义务公式进行的LTL可满足性检查
    5.3 基于SAT的加速技术
    5.4 实验仿真
    5.5 本章小结
第六章 LTL_f的可满足性检查
    6.1 背景介绍
    6.2 从LTL_f到LTL的可满足性规约检查
    6.3 LTL_f迁移系统
    6.4 基于LTL_f有限属性的可满足性检查
    6.5 优化技术
    6.6 实验仿真
    6.7 本章小结
第七章 工具的开发与使用
    7.1 工具的产生背景
    7.2 工具的简单介绍
    7.3 工具的性能测试
    7.4 工具的使用说明
    7.5 小结
第八章 总结与展望
    8.1 全文小结
    8.2 未来工作展望
参考文献
致谢
攻读博士学位期间发表论文和参与科研情况



本文编号：3903051