基于Petri网的on-the-fly模型检测

论文摘要

Petri网是一种重要的数学模型,它能够有效地对并发系统进行描述和建模。线性时序逻辑LTL则是描述和验证并发系统特性的一种重要的形式化工具,它能够方便、准确地描述并发系统的重要性质,如安全性和活性。自动机理论在模型检测中起着非常重要的作用,模型检测是时序逻辑和自动机理论的有机结合,是关于系统性质验证的算法和方法,它通常采用搜索状态空间的方法来检测一个给定的系统模型是否满足某个用时序逻辑公式表示的特定性质。系统模型的状态空间爆炸问题就是模型检测所面临的主要问题。本文详细地描述了Petri网、线性时序逻辑、Büchi自动机、Petri网的可达图和自动机的交自动机,并详细探讨了在基于线性时序逻辑和自动机理论的Petri网的可达图的模型检测策略的基础上,引入了on-the-fly技术来进行Petri网的模型检测。在on-the-fly模型检测中,事先仅需要构造被验证性质对应的自动机和系统的Petri网模型,在对状态空间的搜索中按照双DFS算法的需要动态地构造Petri网的状态可达图和性质自动机的交自动机,与此同时,利用性质自动机来引导Petri网的状态可达图进行动态地构造。这样,在找到被验证性质的一个反例之前,可能仅需要构造交自动机和状态可达图的部分甚至是一小部分的状态空间,从而避免了对交自动机的整个状态空间的穷尽搜索,来尽可能地减少搜索的状态空间,以此来减缓状态空间爆炸的问题。并且存储Petri网模型的可达图以及可达图和性质自动机的交自动机所占用的空间也会减少,从而也可以很好地缓解内存不足的问题。

论文目录

• 摘要
• Abstract
• 第1章 绪论
• 1.1 引言
• 1.2 模型检测
• 1.2.1 模型检测产生的背景
• 1.2.2 模型检测概述
• 1.3 研究内容与本文组织
• 第2章 Petri网及其可达图
• 2.1 Petri网的直观理解
• 2.2 Petri网的形式化描述
• 2.2.1 网及其图形表示
• 2.2.2 P/T系统及其相关定义
• 2.3 抑制弧Petri网
• 2.4 Petri网的可达图
• 第3章 线性时序逻辑与自动机理论
• 3.1 线性时序逻辑LTL
• 3.1.1 LTL的语法
• 3.1.2 LTL的语义
• 3.1.3 LTL公式的NNF形式
• 3.2 自动机理论
• 3.2.1 Büichi自动机
• 3.2.2 泛Büchi自动机
• 3.2.3 标记的泛Büchi自动机
• 3.3 LTL公式到自动机的转换
• 3.3.1 数据结构
• 3.3.2 LTL转换为自动机
• 3.4 交自动机
• 3.4.1 交自动机的定义
• 3.4.2 交自动机的构造算法
• 第4章 on-the-fly模型检测
• 4.1 模型检测的步骤
• 4.2 基于自动机的模型检测
• 4.2.1 基于Petri网的自动机模型检测
• 4.3 双DFS算法
• 4.4 on-the-fly模型检测
• 4.4.1 on-the-fly模型检测概述
• 4.4.2 基于Petri网的on-the-fly模型检测
• 第5章 实例分析
• 5.1 互斥算法
• 5.2 实例的Petri网模型
• 5.3 实例并发特性的描述
• 5.4 性质LTL公式转换到自动机
• 5.5 用自动机进行模型检测
• 5.6 采用on-the-fly技术进行模型检测
• 第6章 总结与展望
• 参考文献
• 在学期间发表的学术论文
• 致谢