基于多值决策过程的广义可能性多值时序逻辑模型检测

论文摘要

模型检测（Model Checking）是一种重要的形式化验证方法,广泛用于软硬件系统行为的自动验证.为了使包含非确定性信息、不完全信息和不一致信息的并发系统得到有效验证,在时序逻辑（Temporal Logic）和决策过程（Decision Process,DP）的基础上,本文研究了具有多值决策过程（Multi-valued Decision Process,MvDP）的广义可能性多值时序逻辑模型检测算法,以及在非确定性系统验证中的应用.首先构造了刻画系统模型的MvDP,引入描述系统属性的多值时序逻辑,然后给出基于MvDP的广义可能性多值时序逻辑模型检测算法.该算法利用决策过程中的调度,将模型检测问题转换为多项式时间内的模糊矩阵运算或模糊矩阵不动点计算.得到的多值计算树逻辑（Multi-valued Computation Tree Logic,MvCTL）模型检测算法的时间复杂度为O（size（M）·|Φ|）,多值线性时序逻辑（Multi-valued Linear Temporal Logic,MvLTL）和多值分支时序逻辑（Multi-valued Branching Temporal Logic,MvCTL*）模型检测算法的时间复杂度均为O(size（M）·exp(|（φ|）.本文的主要工作如下:1.构造MvDP作为有限状态系统的模型.给出MvDP和MvDP上调度的定义,并讨论状态转移、前驱和后继状态、有穷和无穷路径的形式化表示;讨论多值决策过程的初始分布、状态转移分布等相关概念的矩阵表示;给出基于MvDP建模,路径上可能性测度的定义和有穷路径柱集的定义,并给出有穷路径柱集的矩阵表示.2.给出多值时序逻辑的语构和语义.分别给出MvCTL、MvLTL、MvCTL*的语构定义,继而讨论这三种时序逻辑在可能性测度和必然性测度下的语义解释并分别给出语义的归纳定义,讨论了MvLTL的语言语义和路径语义在可能性测度下的等价性.3.给出基于MvDP的广义可能性多值时序逻辑模型检测算法.首先给出算法的问题描述并给出子公式个数的递归定义;然后讨论了“O”,“（?）”,“（?）≤n”等MvCTL时序算子的矩阵计算方法,以及“□”算子,“（?）”算子和“◇”算子的不动点计算方法,并给出基于MvDP的广义可能性MvCTL模型检测算法（GPo-MvCTL算法）并讨论其时间复杂度;接下来,讨论MvLTL的几种特殊可达事件的可能性测度求解,结合MvLTL PNF的语构和语义,给出基于MvDP的广义可能性MvLTL模型检测算法（GPo-MvLTL算法）并讨论其时间复杂度;最后,结合基于MvDP的广义可能性MvLTL和MvCTL模型检测算法,给出基于MvDP的广义可能性MvCTL*模型检测算法（GPo-MvCTL*算法）并讨论其时间复杂度.

论文目录

• 摘要
• Abstract
• 前言
• 第1章 预备知识
•   1.1 经典时序逻辑
•     1.1.1 Kripke结构
•     1.1.2 计算树逻辑（CTL）
•     1.1.3 线性时序逻辑（LTL）
• *）'>    1.1.4 分支时序逻辑（CTL^*）
•   1.2 格理论和多值逻辑
•   1.3 格值可能性测度理论
•   1.4 Knaster-Tarski不动点定理
• 第2章 多值决策过程
•   2.1 多值决策过程
•   2.2 多值决策过程的矩阵表示
•   2.3 基于可能性测度的多值决策过程
• 第3章 多值时态逻辑及其广义可能性测度下的语义
•   3.1 多值计算树逻辑（MvCTL）
•   3.2 多值线性时态逻辑（MvLTL）
• *）'>  3.3 多值分支时态逻辑（MvCTL^*）
• 第4章 基于MvDP的广义可能性多值时序逻辑模型检测
•   4.1 广义可能性MvCTL模型检测
•     4.1.1 MvCTL时态算子的计算方法
•     4.1.2 GPo-MvCTL模型检测算法
•   4.2 广义可能性MvLTL模型检测
•     4.2.1 MvLTL各算子的计算方法
•     4.2.2 几种特殊线性性质
• *模型检测'>  4.3 广义可能性MvCTL^*模型检测
•     4.3.1 MvLTL PNF的语构和语义
•     4.3.2 GPo-MvLTL模型检测算法
• *模型检测算法'>    4.3.3 GPo-MvCTL^*模型检测算法
• 总结
• 参考文献
• 致谢
• 攻读硕士学位期间科研成果

文章来源

类型: 硕士论文

作者: 袁申

导师: 李永明

关键词: 模型检测,多值逻辑,广义可能性测度,决策过程,时序逻辑

来源: 陕西师范大学

年度: 2019

分类: 基础科学

专业: 数学

单位: 陕西师范大学

分类号: O225

DOI: 10.27292/d.cnki.gsxfu.2019.000632

总页数: 69

文件大小: 2317K

下载量: 6