概率逻辑的限界模型检测技术

概率逻辑的限界模型检测技术 分类号. 密级 坌五 . 编号 ?江薄大擎 硕士学位论文 概率逻辑的限界模型检测技术 申请学位级别 专业名称 亟? 让篁扭应用撞查 论文提交期 论文答辩期 呈生曼旦 至呈生鱼旦皇旦 学位授予单位和期 江菱太堂 圣生鱼旦 答辩委员会主席 图美 评词人独创性声明 本人郑重声明:所呈交的学位论文,是本人在导师的 指导下,独立进行研究工作所取得的成果。除文中已注明引 用的 内容 财务内部控制制度的内容财务内部控制制度的内容人员招聘与配置的内容项目成本控制的内容消防安全演练内容 以外,本论文不包含任何其他个人或集体已经发表 或撰写过的作品成果。对本文的研究做出重要贡献的个人和 集体,均己在文中以明确方式标明。本人完全意识到本声明 的法律结果由本人承担。 学位论文作者签名:叶萌 日期:切’年‘月眵日学位论文版权使用授权书测掣掣弊 本学位论文作者完全了解学校有关保留、使用学位论文 的规定,同意学校保留并向国家有关部门或机构送交论文的 复印件和电子版,允许论文被查阅和借阅。本人授权江苏大 学可以将本学位论文的全部内容或部分内容编入有关数据 库进行检索,可以采用影印、缩印或扫描等复制手段保存和 汇编本学位论文。 保密 口,在 年解密后适用本授权书。 本学位论文属于 团。 不保密 学位论文作者签名:叶辐 指导教师签名:用‖彳 。 年月日 如/,年‖月/多日江苏大学硕士学位论文 摘 要 模型检测是一种自动化程度非常高的有限状态系统验证技术,目前已经在计 算机硬件、通信与安全 协议 离婚协议模板下载合伙人协议 下载渠道分销协议免费下载敬业协议下载授课协议下载 、软件可靠性的验证方面获得了较大的成功。传统模 型检测技术关注的是系统行为的绝对正确性,如系统不能进入死锁状态。然而分 布式算法,多媒体协议,容错系统等往往关心某种量化属性,如消息传送失败的 概率不高于%,在时间内至多个消息丢失的概率不高于.%,请求发送后在 个时间单元内得到响应的概率不低于%等等。随机模型检测致力于解决这 类属性的自动化验证问题。 在随机模型检测中一般使用概率计算树逻辑和连续随机逻辑刻 画属性,使用马尔科夫过程,概率时间自动机等建立系统模型。与传统模型检测 一样,状态空间爆炸问题也是随机模型检测技术实用化的主要瓶颈。在为缓解状 态空间爆炸问题已经提出的诸多理论和方法中,限界模型检测技术是克服状态空 间爆炸问题的最为有效的方法之一。本文主要工作是提出了概率奖励计算树逻辑 和概率实时认知逻辑的限界模型检测技术,具体包括以下两个方面: .概率奖励计算树逻辑以离散时间马尔可夫链作为系统模型,为缓解该模 型上的状态空间爆炸问题,提出了概率奖励计算树逻辑的限界检测技术。首先定 义概率奖励计算树逻辑的限界语义,并证明其正确性;其次提出基于线性方程组 求解的限界模型检测算法;然后通过实例说明了限界模型检测的过程。最后在概 率奖励计算树逻辑的基础上提出了重复可达性和持续性的限界语义和限界模型 检测算法,并以实例来说明限界模型检测的过程。实验结果表明在属性成立的证 据较短的情况下,限界模型检测能够快速的完成验证。 . 为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了 概率实时认知逻辑。模型检测是验证多智体系统是否满足 公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈。为此提出一种 的限界模型检测算法。首先,将的模型检测问题转换为无实 时算子的的模型检测问题;其次,定义的限界语义,并证明其 正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概 率 度量序列的演化规律和数值计算中牛顿迭代法使用的迭代过程终止判断准则,设 计了一系列的限界检测终止性判别准则,并分析了各种准则适用的场景。此外还概率逻辑的限界模型检测技术 针对线性方程组的特点,给出了变元求解的次序,从而避免不必要的迭代运算。 实例研究表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模 型检测完成验证所需空间更少。 关键字:模型检测,限界模型检测,概率奖励计算树逻辑,概率实时认知逻辑, 状态空间爆炸江苏大学硕士学位论文 , , ,. , ., , ,, %. .%.%, . . , , . , . , .. . . ., ., , ., . ,. ., . .. .? ,. .? 概率逻辑的限界模型检测技术 . . .,.,. , .,, , , . .: , ,,,江苏大学硕士学位论文 目 录 第一章绪论 .研究背景?.. .研究现状?.. .研究内容及论文组织??。 第二章相关的概念 .概率分布与度量.离散时间马尔可夫链 .概率计算树逻辑?一 .马尔可夫链奖励模型??.. .概率时间自动机?. .概率时间自动机的平行组合??. 第三章概率奖励计算树逻辑的限界模型检测一 .概率奖励计算树逻辑..概率奖励计算树逻辑的语义??一 ..概率奖励计算树逻辑的等价性?.. .概率奖励计算树逻辑的限界语义 .概率奖励计算树逻辑的限界模型检测算法.实例:零配置协议? .测试结果?。 .重复可达性和持续性..重复可达性和持续性的语义??一 ..重复可达性和持续性的限界语义.. ..重复可达性和持续性的限界模型检测算法 ..实例研究?.. .本章小结? 第四章多智体系统中约简状态空间的限界模型检测算法?一 .概率实时解释系统. .概率实时认知逻辑..概率实时认知逻辑的语法??. ..概率实时认知逻辑的语义??. .概率知识区域图? .基于概率知识区域图的限界模型检测?. ..时态逻辑的转换?.. .. 的限界模型检测?.. .. 的限界模型检测算法??一 .线性方程组的求解 .实例研究?. ..火车穿越控制系统一 ..限界模型检测算法一 概率逻辑的限界模型检测技术 .终止性选择 标准 excel标准偏差excel标准偏差函数exl标准差函数国标检验抽样标准表免费下载红头文件格式标准下载 ? .本章小结?. 第五章结论与展望??.. .结论.展望参考文献? 致谢?.. 攻读硕士学位期间发表的论文? 江苏大学硕士学位论文 第一章绪论 .研究背景 模型检测【自二十世纪八十年代提出以来,已经变成了最成功的自动化验 证技术之一。它是一种有限状态系统验证技术,因其自动化程度高,逐渐引起 了 广泛的关注。目前模型检测被广泛应用于硬件、通信协议、安全协议、分布 式算 法的正确性证明与可靠性分析,例如 利用模型检测技术成功地验证 了微处理器的乱序执行单元【和多处理机的一致性协议【, 等验证了/协议和 协议。在模型检测中,系 统一般被模型化为一个有穷状态转换系统,如结构、有界网等,检 测的属性一般利用时态逻辑公式描述,典型的如计算树时态逻辑 【,线性时态逻辑 【。 模型检测主要通过遍历有穷状态转换系统的全局空间来验证属性是否成立。 模型检测的基本思想是当验证某一系统是否满足属性尸时,把该系统建 模成一个相对应的马尔可夫模型。,用逻辑公式?。来表示要检测的属性。这样 验证系统是否满足属性尸就转化成了验证马尔可夫模型。是否满足逻辑公式 矽。的模型检测问题,即 ?。是否成立。这样就可通过模型检测工具按照特定 的模型检测算法对该属性自动验证。常用的模型检测工具有、、 们以及实时模型检测工具?、等。若验证系统满足属 性时,则会返回真值,若系统不满足属性时,模型检测工具会给出一个不满 足该属性的实例,通过对实例的研究来分析属性不成立的原因。 计算树逻辑和线性时态逻辑都是属性规范描述语言,利用模型检 测算法验证系统是否满足计算树逻辑和线性时态逻辑的属性规范,对确保系统的 可靠性具有重要的意义。这两种时态逻辑可以规范系统行为的绝对正确性,如系 统运行不可能失败。然而实际生活中有很多随机现象,比如在不可靠信道上传递 消息导致的消息丢失,对这一类现象往往更关心某种概率度量,如消息传送失败 的概率不高%等等。对这类属性计算树逻辑和线性时态逻辑是无法刻画的,因 此研究人员在计算树逻辑和线性时态逻辑的基础上引入了概率算子,得到了概率概率逻辑的限界模型检测技术 计算树逻辑】等规约形式,并提出了相应的概率模型检测方法【】。在概 率计算树逻辑中引入奖励算子,得到了概率奖励计算树逻辑】。实际生 活中我们会遇到验证系统的重复可达性和持续性的情况,因此在概率奖励计算树 逻辑的基础上进行了修改,得到了概率奖励计算树逻辑的规约形式。 知识推理】一直是多个领域的研究人员积极探索的课题,比如哲学、经济、 人工智能、分布式系统等。特别是在分布式系统领域,时态认知逻辑【能更准 和 提出利用 确地描述系统和协议的规范,因此自年 模型检测技术完成时态认知逻辑的演绎推理【 】之后,模型检测时态认知逻辑一 直是一个重要的研究领域,并且在多智体系统中得到了广泛的应用,例如在文献 等将每一个保密家视为一个智体,就餐的多位保密家构成了一 中 个多智体系统,使用时态认知逻辑刻画了协议的匿名性,利用模型检测技术判断 出逻辑公式成立,从而验证了保密家协议的匿名性,在文献中骆翔宇等将铁 路控制系统视为一个多智体系统,利用模型检测技术验证了控制系统的活 性。 模型检测时态认知逻辑的研究主要围绕三个方面进行,包括模型检测算法、 系统和属性规范、状态空间约简技术。给定一个系统模型和一个逻辑公式描述的 属性规约,检测算法主要判断系统是否满足规约,例如 提出了一种将 时态认知逻辑的模型检测问题转化为模型检测问题的方法【。规范 主要研究不同特性的逻辑刻画,基本的认知时态逻辑包括】, 然而在实际的应用中,有时必 须考虑实时性,比如在火车穿越控制系统中,火车进站的信号发出后安全门必须 在秒内关闭等等,为此 等学者提出了实时认知逻辑。 在另外一些重要领域,对某些事件发生的可能性进行推理也比较重要,比如“事 件发生的概率小于/”, “在请求发出之后两秒内得到响应的概率不低于 %”等等。这些规范可以通过在时态认知逻辑中引入表示概率分布的算子得到 表示,为此等学者提出了概率认知逻辑, 等提出了概率认知逻辑?。本文提出一种概率实时认知逻辑 ,从而可以对概率、实时以及知识进行推理。 模型检测是基于对系统状态空间的穷举搜索,系统的规模随着并发分量的增 加,呈指数级增长,因此当一个系统的并发分量较多时,那么状态空间是无限的江苏大学硕士学位论文 或是非常大的,这样就可能得不到验证结果或不能在有限时间内得到结果,从而 模型检测的执行效率会受到的严重影响。系统的状态空间在并发系统中会随着并 发分量的增长而呈指数级别的增加。由于时间连续的属性,在实时系统中会有无 数个具体的状态,这将导致状态空间是无限的,这就是所谓的状态空间爆炸问题 】。状态空间爆炸问题是制约模型检测发展应用的一个瓶颈。因此,如何缓解 模型检测中状态空间爆炸问题,是充分应用模型检测、提高模型检测效率的关键。 与传统的模型检测一样,概率奖励计算树逻辑模型检测和概率实时认知逻辑模型 检测也面临着状态空间爆炸问题。因此,如何缓解概率奖励计算树逻辑和概率实 时认知逻辑模型检测中的状态空间爆炸问题是需要解决的重要问题,这对于提高 这两种逻辑模型检测的效率,使其变得实用性是具有非常重要的理论意义和现实 意义。 .研究现状 多年来许多学者都对状态空间约简技术做了相关的研究,主要包括符号化计 算四、抽象【】、偏序归约、限界检钡等等。年 首次提出将 的模型检测问题转换为命题公式的可满足性判定问题【,这被认为是限界模 型检测的起源。限界模型检测的基本思想是只遍历足以用来验证某一规范的部分 状态空间,优点是不会遇到状态爆炸问题,并且能够快速获取最小长度的反例, 内存消耗远小于基于有序二叉决策图的方法,而且无须对变量进行静态或动态排序。 。 年 将限界检测技术应用于的全称片断的验证【 年, 等进一步提出了多智体系统中验证时态认知逻辑 的全称片断的限界模型检测方法【 ,并开发了相应的限界检测工具。 等在时态逻辑的语言中引入认知模态词,得到一个新的时态认知 。 逻辑,并展示了相应的限界模型检测算法【 等将实时性引 入到认知逻辑中,得到了一种实时认知逻辑,并提出了的限界模 型检测算法【。 上述不同逻辑系统的限界检测本质上是为验证的属性寻找反例的过程,并将 反例的存在性转换为命题公式的可满足性判定问题。造成能够转换为命题公式可概率逻辑的限界模型检测技术 满足性判定问题的关键在于这些反例仅仅涉及状态转换,转换关系可以用命 题公 式编码。而概率算子的反例由于在路径的转换过程中涉及概率度量,利用命题公 式很难进行编码。因此概率算子的限界检测有很多新的特性,这些新特性使得我 们必须对概率算子的限界检测进行系统的研究。 举例如下,公式尉的证据是一条有穷路径%,‘,...,矗,其中墨满足?,因此只 需对薯,瓯,之间的转换关系以及吼满足?进行编码。而对于公式.。彩,证据是 ‘ 路径的集合,比如%与‘?毛,%与‘?屯,其中是,屯满足矽。因为事 先无法预知状态之间的转换概率,所以无法计算集合当中包含多少条路径,从而 无法使用命题公式编码。 此外传统的限界检测中会对路径的长度设置一个界,使得如果存在反例必存 在长度不超过界的反例,从而保证了限界检测技术的完备性。但是对于概率算子 这种方法将失效,考察图.所示的例子,验证的属性是初始状态。是否满足 。矽。很明显‰满足足。?,但是随着步长的增加从步长开始我们得到这 样一个概率度量序列。,了,,万,虿,万,万,...一纠引,...因此在事先不能确定是否已 经遍历全局空间的情况下,无论步长如何增长始终不能得到真实的概率度 量。 此实例说明以设置路径长度的上限作为判断算法终止的标准已经失效,必须设计 新的标准等等。总之概率度量算子为限界检测技术带来了很多新的问题,论文将 对这些新问题进行详细的研究。 图.一个简单的概率转换系统 .研究内容及论文组织 本文主要研究概率奖励计算树逻辑和概率实时认知逻辑的限界模型检测,包 括概率奖励计算树逻辑的限界模型检测的研究、重复可达性和持续性的限界模型 检测的研究以及概率实时认知逻辑的限界模型检测的研究。江苏大学硕士学位论文 具体研究内容如下: 概率奖励计算树逻辑是在概率计算树逻辑中加入了奖励 的概念。提出了概率奖励计算树逻辑的限界模型检测技术,来缓解概率奖励计算 树逻辑模型检测中的状态空间爆炸问题。首先刻画了概率奖励计算树逻辑的限界 语义,并证明其正确性,并将公式的限界满足性关系转换成线性方程组 求解。然后通过实例说明了限界模型检测的过程。最后在概率奖励计算树逻辑的 基础上提出了重复可达性和持续性的限界语义,对这两个属性的满足性检查同样 转换成线性方程组求解,并通过具体的例子来说明两个属性的限界模型检测过 程。实验结果表明在属性成立的证据较短的情况下,限界检测能够快速的完成验 证。 概率实时认知逻辑是在概率认知逻辑中加入了实时算 子。提出了概率实时认知逻辑的限界模型检测技术,来缓解概率实时认知逻辑模 型检测中的状态空间爆炸问题。先将的模型检测问题转换为无实时算 子的概率分支认知逻辑 的模型检测问题。定义了的限界语义,并证明了其正确性。 设计了基于线性方程组求解的限界模型检测算法,即将的限界模型检测 问题转换为线性方程组的求解问题。说明以路径长度作为检测过程终止的判别条 件已经失效,我们基于数值计算中牛顿迭代法使用的迭代过程终止判断准则,设 计了一系列的终止性判别准则,并分析了各种准则适用的场景。另外针对线性方 程组的特点,给出了变元求解的次序,从而避免不必要的迭代运算。实例研究表 明,与传统的限界模型检测一样,的限界模型检测是一种前向搜索状态 空间的方法,在属性为真的证据较短的情况下,完成验证所需内存空间较少。 论文如下组织: 第一章对模型检测的产生背景、基本思想以及概率计算树逻辑和概率时态逻 辑模型检测中面临的状态空间爆炸问题进行概述,以明确主要研究内容。 第二章介绍了离散时间马尔可夫链、概率计算树逻辑和引人奖励的概率而得 到的马尔可夫链奖励模型的概率。以及概率时间自动机等相关概念, 第三章对概率奖励计算树逻辑的限界模型检测技术进行了系统的探讨。定义 了的限界语义,并且证明其正确性。将的限界模型检测问题转 换为线性方程组的求解问题。通过具体实例零配置协议说明了限界概率逻辑 的限界模型检测技术 模型检测的过程。对进行了扩展得到了重复可达性和持续性的限界语义, 并且证明其正确性,通过两个测试用例说明了这两个属性的限界模型检测的 过 程。 第四章研究概率实时认知逻辑模型检测的限界模型检测技术。将 的模型检测问题转换为无实时算子的的模型检测问题。定义了 的限界语义,并证明了其正确性。将的限界模型检测问题转换为线性方 程组的求解问题。最后通过实例火车穿越控制系统来说明限界检测的过程。 第五章对本文进行了 总结 初级经济法重点总结下载党员个人总结TXt高中句型全总结.doc高中句型全总结.doc理论力学知识点总结pdf ,并给出了对下一步研究的展望。江苏大学硕士学 位论文 第二章相关的概念 本文中会涉及到一些理论知识和基本概念,本章主要对后面章节中所要用到 的这 些基本理论知识进行简要的介绍。 .概率分布与度量 定义概率分布【可数集合上概率分布‖是一个到【,】的映射函数, 且满足?‖。 ? 记号表示集合上概率分布的集合。记号 】表示中的元素上的 点分布,即】?,且墨】。一项随机试验中所有可能发生的结果 形成的集合称为样本空间,记为。中的元素称为基本事件,的子集称为事 件,样本空间称为必然事件,空集。称为不可能事件。在实际问题中,我们不 是对所有的事件样本空间的所有子集感兴趣,而是关心某些事件的某些 子集及其发生的概率,从而形成盯代数的概念。集合??称为上的盯代数, 当且仅当 》 ??: 》 如果?,则\?; 如果巨,,...?,则巨?。 定义.概率空间概率空间【是一个三元组:,,,这里为样本 空间,集合为上的盯代数,:斗,】是度量函数,满足下面三个条件: 对任意的??,??; ; 对?中两两不相交的事件易,...,甚。巨?羔。。 对于,称其中的任何元素是可度量的。概率逻辑的限界模型检测技术 .离散时间马尔可夫链 离散时间马尔可夫链是一簇随机变量料七 ,?.,这里七是在每一个 离散步的观察。七的取值称为状态,状态空间的集合是离散的。离散时间马 尔 可夫链必须满足马尔可夫性质,即七仅仅依赖于一,而与,...,一无 关。另外我们考虑的离散时间马尔可夫链是齐次的,这意味着状态之间的转 换概 率独立于时间。因此给出状态之间的转换概率就足够描述离散时间马尔可夫 链。 定义离散时间马尔可夫链,,,印,三是一个五元组,这里 是有限状态集; :×一【,】是转换概率函数,且满足对任意的状态?,, ; ?是初始状态; 却是有限的原子命题集; :寸却是标记函数; 直观上,一个离散时间马尔可夫链是一个所有转换关系附上离散概率的 结构。 定义路径设为离散时间马尔可夫链,中的路径万是一个无穷 状态序列,,.一使得,双薯,薯,。 为了表达表达方便,引入记号表示从状态出发的路径集合,对于路 径,,?,引入万表示万上的第个状态。对于离散时间马尔可夫链和 状态, 令 这里 ,为盯代数定义为 ?’, 。 上 的 概 万 是刀的有限前缀 率 度 量 定 义 为 ,。,:,?%?尸‘,墨,,这里。。这样我们从离散时间马尔可夫链和 蔓? 状态演绎出一个概率空间。江苏大学硕士学位论文 .概率计算树逻辑 概率计算树逻辑是基于的分支时态逻辑。由状态公式和路 径公式组成,分别在马尔可夫链的状态上解释状态公式,在路径上解释路径 公式, 和的主要区别在于去除了全称和存在路径量词,引入了概率算子 只妒,这里妒是路径公式,是【,】上的某个区间。的形式化定义如下: 定义.概率计算树逻辑,原子命题集却上的状态公式: ?孬晚磊织一缈弓 这里口?,是一条路径公式,?【,】是以有理数为边界的区间。 路径公式: 缈::爿矽??萌欢破磁 这里?,破,欢是状态公式。 为了方便起见不再显示书写区间,而是使用简写,例如用罡?妒表示彳叩, 妒, 罡,够表不墨?】。 .马尔可夫链奖励模型 除了研究某些事件的概率,有时候还需要分析马尔可夫链一次执行中的平均 行为。比如在一个通信系统中,发送者通过一条不可靠的信道向接收者发送消息, 衡量发送消息的预期次数是我们感兴趣的。换句话讲,当离开某一状态时我们 会得到一个与相关的值,我们将这个值称为奖励。例如当离开消息的发送者时 会得到的奖励值为,说明尝试发送消息为次。对于要附加奖励的马尔可夫链 称为马尔可夫链奖励模型。 定义 是一个二元组?,,其中是状态空间为的马尔可夫 链,是一个奖励函数,它给每一个?的状态分配一个非负整数,.。对于 路径茹%?晶,,.洲定义为 ...。一 由于路径茹没有离开霸,%的奖励值不用考虑。 概率逻辑的限界模型检测技术 定义.?,是,是状态空间,?是目标状态集,万。屯? 是的一个无穷路径,定义 ? 盯厅? ,.,科一晶’瓣警加硼删%印 这里,.刚万,表示沿着无穷路径/第一次到达中的状态的累积奖励。 定义奖励的期望值如果 似则馏,如果 则 ??‘万?:/,, 或者 ?尸万? 茹是所有&,?..晶的有限路径,且%?,%,%,..??仨。 在中求到达一个给定的状态集的概率时,通常会事先给出累积奖励的 边界值叫做可达概率的花费边界。若一条路径在到达目标状态时超过了累积 奖励 的边界,就认为花费过大。 定义令?,,.是正整数,表示到达目标状态集的累积奖励最多 为,.,它的概率为 似:,?,. ?。,‘刀?万 .概率时间自动机 时间自动机【用于为实时要求较高的系统进行建模,本质上是一个状态转换 系统。概率时间自动机是对时间自动机的概率扩展,可以描述行为具有不确 定性 的系统。由于时间自动机中涉及到时问因素,在给出它的概念之前,先介绍一 下 时钟约束、时钟赋值的概念。 定义.时钟约束 定义时钟变量集合上的一个时钟约束的语义 ? ? 为:: / .其中,?,?是一个时钟变量。 我们用来表示在时钟变量集合上的所有时钟约束的集合。江苏大学硕士学位 论文 定义.时钟赋值 时钟变量集合上的一个时钟赋值是一个函数 专恐。,它为每个时钟变量?指定一个当前值,。用表示时钟 变量集合上的所有时钟赋值的集合。 定义.令:【,?为非负实数的集合,,?..为自然数的集合,是 有限时钟集,:专为时钟赋值,是时钟集上的赋值集合。令?,形式化定义为 : ,。令?,::?形式 化定义为:?,:,?\,:】’,。时钟约束刻画了对 时钟的约束,形式化定义为::仃? ?. ,这里 , ,,?。上时钟约束的集合定义为域,记为。时钟约束和时 钟赋值的满足性关系定义如下: 》 ; ?当且仅当,?; 》?当且仅当?; ?当且仅当?; ,当且仅当?; 岛当且仅当卜氧或者幺; 》 幺乞当且仅当厶且乞 定义.概率时间自动机【】概率时间自动机是一个八元组 ,,,,,,, ,其中: 是有限的位置集合; 》 ?是初始位置; 》 是时钟的集合; 》 是有限的动作集合; : 一是每个位置应该满足的不变量条件; 》 :×?是动作触发应该满足的条件; :。眈“是概率转换函数;概率逻辑的限界模型检测技术 :三斗却是位置标记函数,其中和是原子命题集合。 在概率时间自动机中时间的流失和动作的执行均可导致系统的状态发生变 化。开始时系统处于初始位置,所有时钟的初始值为,并且以统一的速率增 加。概率时间自动机上的状态是一个满足胁,的二元组,,?。在任何 状态,,下时间会自动流失,然后在某个时间点系统执行动作口?,从而导致 系统所处的位置发生变化。时间的流失必须保证不能失效。对于动作口?, 只有当满足,口时才能被选择执行。一旦执行动作口,某个时钟集合将会 被重置,后继的位置依据分布,口随机选择。 图.显示的是一个不可靠信道上的简单通信协议的概率时间自动机模型。 系统由发送者和接受者两个主体组成,主体之间通过一个信道以及全局时钟工, 进行通信。消息的传递认为是瞬时的。初始状态设定为新的数据到达发送端, 此时,的值设定为。发送者将数据保留到个时间单元,然后发送数据, 同时将的值设置为。数据成功到达接收端的概率是.。接收端在接受到数 据之后必须在一个时间单元内给发送者发送消息到达的确认信息。确认信息成功 到达发送端的概率是.。一旦确认信息到达接收端,在下一个数据包到达发送 端之前,时间可以任意流失。但是如果数据包丢失了,接受端将处于空闲状态, 而发送端会一直处于等待确认信息的状态。因此,发送端将在发送信息之后的 到个时间单元内重新发送消息。如果消息重发多于个时间单元或者接受端接 受到了数据,本次信息传递过程结束。 现在说明图.中原子命题表达的含义。发送端共有四个状态:接收到数据 包,发送数据后等待数据确认信息,接收到确认信息,终止, 分别用原子命题 ,,,表示。接受端共有三个状态:空闲,接收 到数据,终止,分别用原子命题犰,,已口,,口表示江苏大学硕士学位论文 图.一个简单通信协议的概率时间自动机模型 .概率时间自动机的平行组合 对于 定义 分布 分布。?舶×厶 ,:?:×厶 :?删加×厶× :如下:对于任意的?石,五 筋,?厶,,?上:,令 。: :,,,?::,乞。引入记号,,卜?表示×厶上的一 种特殊概率分布: , ,‘,对任意的。?彩五?石, ,?厶, 囝,‘ 一,功。引入记号?,,卜?表示上的一种概率分布: 囝,乞 ,乞,对任意的:?:?以,,?三:,?, :,。 定义 . 概率时间自动机的平行组合【令 只厶,,石,,,,帕,,,,?,为两个概率时间自动机,石:。鼻, 只的平行组合定义为只 厶×百,一,而屁,彳 :,,,, ,其中: 》对任意的,,,:?厶×上:,,。:,; :厶××爿 斗 定义如下: ?\,,,口,口; 概率逻辑的限界模型检测技术 口?彳吒\,,,,口,口; 口?爿 :,,,,口,,口; ?,乞,口当且仅当下面三个条件中的一个成立: \,存在?,口使得 ,,?; 口?\,存在?,口使得,,卜?圆:; 口?彳%,存在?,口,?,口使得。 粤,,,粤,。 ? 』? 郇、,、., ,?,,: 、~一,, 墨竺 哄锈、、~ 、一一 图概率时问自动机弓 图概率时间自动机忍 图,分别给出了两个简单的概率时间自动机鼻,只,现在考察暑与 的平行组合暑昱。对于初始位置厶,, :。,在只中初始位置厶。下口是唯一 可以被 触发的动作,在只中初始位置厶。下是唯一可以被触发的动作。因为口?\, 所以口的执行会导致弓的状态发生变化,只的状态保持不变。对于动作,因为 ?:\,所以的执行会导致只中的状态发生变化,鼻中的状态保持不变。 在鼻中口的执行导致位置变为厶:的概率是.,变为厶,的概率是.,因此在口 中执行动作口导致厶。, ,.变为三?三:。的概率是.,变为厶,,。的概率是.。 在只中的执行导致位置变为。的概率是.,变为:的概率是.,因此在曰 中执行动作导致厶。, :。变为‰ 。,的概率是.,变为厶。,上::的概率是.。 上述考察的动作口和在厶,,:。下执行只能导致一个位置发生变化,而对于位 置 江苏大学硕士学位论文 厶:,。,执行动作会导致两个位置同时发生变化。在厶:下执行导致位置从三: 变为厶,的概率是.,。下执行导致位置从厶。变为厶:的概率是.,因此在 厶:,。下执行导致位置变为厶,,:的概率是.。同样的,变为厶:,:的概率 是.,变为厶,,三:。的概率是.,位置不发生改变的概率是.。依据定义, 最终的平行组合日 如图所示。 图?概率时间自动机日,的平行组合日最 定义‘一个马尔科夫决策过程肘是一个五元组,一,彳砌疗,脚,三口“,其 由 》是状态集; ;?是初始状态: 》 是动作集; :×一’印是概率转换函数: 》:一和是状态标记函数,其中却是原子命题集合。 图?所示的是一个简单的马尔科夫决策过程.在该过程中,:,‘,:,;是概率逻 辑的限界模型检测技术 初始状态,爿珂口,良,概率转换函数为;,,;:三, ,,,口,。,口;,状态标记函数为, ,?。 在马尔科夫决策过程中,路径是一条有穷的序列,%,%%?,巾,满 足挖一,薯,口‰。称状态是从状态岛可达的当且仅当存在路径 %,,,,口,..~ ,%使得%。 ??,,. ??,, 图.一个简单的马尔科夫决策过程 图最的语义解释 定义.概率时间自动机的语义【令厶,,,,,,粤是一个 概率时间自动机,其语义定义为一个马尔科夫决策过程,;,,,,其 中: ,,?憾。; ,; 豫: ’/, 旯?/,,,口当且仅当对于任意的?’?,, ,口,对任意的北’?: ?。’【:】; 旯,’,’,口,,’ ,粤“。 考察图中概率时间自动机最,设马尔科夫决策过程:是 的语义,如图 所示。在:中初始状态是 :,,。由置中 :。下动作触发的条件可以知道,在: 中动作.,不会导致初始状态发生任何变化,而动作.,的触发会导致状态发 生变化,具体变化是以.的概率变为状态 :。,,.的概率变为状态 ::,。 江苏大学硕士学位论文 第三章概率奖励计算树逻辑的限界模型检测 为缓解概率奖励计算树逻辑模型检测中的状态空间爆炸问题,提出 了概率奖励计算树逻辑的限界模型检测。具体研究内容包括:根据语义等价关 系将转换为概率约束仅为?或者的形式,定义了的限界语 义,并且证明其正确性。摒弃了传统限界模型检测方法中基于命题公式满足性判 定的求解算法,将的限界模型检测问题转换为线性方程组的求解问题。 通过具体实例零配置协议说明了限界模型检测的过程。最后通过三 个测试用例研究限界模型检测算法中模型的边界和线性方程组变量个数之间的 关系。结果表明:界越长,限界模型检测得到的概率度量就越来越逼近真实 的概率度量;限界模型检测是一种前向搜索状态空间的方法,在属性为真的 证据比较短的情况下,能够快速的验证属性;由于奖励的边界的限制,随着 边界值的增加,限界模型检测得到的概率度量的值最终会等于真实的概率度量的 值。 .概率奖励计算树逻辑 概率奖励计算树逻辑是在原来概率计算树逻辑的基础上引入 了奖励的概念。 ..概率奖励计算树逻辑的语义 概率奖励计算树逻辑的形式化定义如下: 定义概率奖励计算树逻辑, 原子命题集却上的状态 公式: ?::. 一?磊政硝欢只缈‰矽 这里口?却,妒是一条路径公式, /?,和是以有理数为边界的区间。 路径公式: 妒::矽 ? 矽萌欢萌破 ;,? ,痧 :,矽萌;,政萌愿,欢 这里?,孬,欢是状态公式,是正整数。 定义.概率奖励计算树逻辑的满足性关系令口?和为原子命题,概率逻辑的 限界模型检测技术 ,,%,和,工是离散时间马尔可夫链,?,破,珐是的状态公式,伊是 的路径公式。对于状态公式满足性关系定义为: 卜当且仅当? ; ,萌当且仅当?识; 卜钨欢当且仅当 破且欢;萌欢当且仅当卜旃或者卜欢; 弓力当且仅当妒?,这里缈耽伽?万妒; 卜最矿当且仅当卜?并且前提是卜?否则 々 这里 黝缈?,.??万々,?讲妒,. 对于中的路径万,满足性关系定义为: 破当且仅当万破; 》 萌当且仅当存在自然数使得万圳稿; 万孬当且仅当对任意的自然数,万圳稿; 万磊欢当且仅当存在自然数/使得万,唬,且对于任意小于,的自然数 ,万稿; 万户稿尺欢当且仅当对任意自然数/使得欢,或者存在自然数使得 万忌稿,且对任意不大于的自然数,万欢; 关于花费边界为,.的算子的可满足性关系与上面类似,只是多了符合的 路径刀满足?,.; ..概率奖励计算树逻辑的等价性 限界模型检测的主要思想是在系统有限的局部空间中寻找属性成立的证据 或者反例。对于概率算子部分,限界语义必须保证属性在有限局部空间 中成立,则在整个运行空间中也一定成立。对于只。这类算子,如果在有限局部 空间中属性成立的概率不小于实数,那么自然的在整个运行空间上属性成立的 概率也不小于。而对于只。这类算子,如果在有限局部空间中属性成立的概率 不大于实数,并不能保证在整个运行空间上属性成立的概率也不大于。为了江苏大学硕士学位论文 保证足,算子限界语义定义的正确性,我们将公式转换为等价的且概率约 束为足,或者只,形式的公式。 定义公式的等价称状态公式仍?是等价的,记为缈兰?, 当且仅当对任意的离散时间马尔可夫链,任意的?,妒当且仅当矽。 不难验证我们有下面的等价关系 芦 只,仍三罡中.仍, 只,够三只.,彳.仍; 芦 ,仍兰足。中、仍, ,仍;只,.仍; 足,仍三足,中、仍, ,仍三只。一,,仍; 芦 芝,仍仍三罡,申?三足。中仍晚 只仍仍三只。中鲲经三只。中一仍尺仍; 户 罡,仍尺仍;罡,中仍仍三 。中、仍、鲠 只,纷尺仍;只中、仍尺仍兰只,中、仍仍。 上述等价关系表明我们只需在的某个子集上讨论其限界模型检测问 题。该子集与具有相同的表达力,且概率约束只能为?或者,将该 子集记为,。即若模型在,集合的有限状态空间中成立,那么它在 整个状态空间中也成立,这是显然的。 .概率奖励计算树逻辑的限界语义 本小节我们将探讨概率奖励计算树逻辑在有限状态空间中的语义。 定义?令口?为原子命题,,?和, 是离散时间马尔可夫链, ?,仍,仍是:的状态公式, 妒是:的路径公式,七,,为自然数称 为界,为了能在全局空间上也成立,这里我们只讨论。乓。妒的情况。状态公 式满足性关系。定义为: 。日当且仅当口?三; 》 。萌政当且仅当。萌且 。唬;。鹕欢当且仅当卜。萌且或者卜。珐;。乏。 咖当且仅当 :;?,这里 ;伊协?万。奶; 。丘。?当且仅当卢。?勋矽?并且前提是卢?黜矽这 . 概率逻辑的限界模型检测技术 里 ?,.??万,?&?,.。 对于中的路径万,满足性关系。定义为: 万。钨当且仅当万。破 卜。矽。; 万;旃当且仅当存在自然数?,使得万圳;?。; 万。萌当且仅当对任意的自然是,乃。?。,且存在自然数?,?是 使得 ,石,,刀万,?,石,,?,万忌。; 刀。萌红当且仅当存在自然数,?,使得万/卜。矽:,且对任意小于,的 自然数,。庐。; 万。识磁当且仅当 ?对任意的自然是?,万圳。矽:,且存在自然数?,?使得 ,万/,万石,?,一万力,?一,乃七。; 或者 ?存在自然数?,使得卜。矽,,且对任意小于的自然数, 万圳女?; 关于花费边界为,的算子的可满足性关系净。与上面类似,只是多了前提, 符合的路径万满足?; 这里要注意的是虽然限界模型检测的路径的前提是有限的,但它仍然是代表 无限的路径,即在它的最后状态有一个回循环到达它的前驱状态。我们使用 的概念来定义限界模型检测中的有界的定义。即上面定义中的自然数, 即为他的循环点的位置。 定理令?却为原子命题,,,。,, 是离散时间马尔可夫链, ?,矽是:状态公式,为自然数,如果净。矽,则卜矽。 证明:对于原子命题及其否定,以及布尔连接词,因它们直观简单,这 里忽略,只讨论足,缈和疋。矽,采用对矽的长度进行归纳的方法来证明结论: 女足.妙说明卜女妒?,即卢?缈‘万?万;妒? .矽 ,叫西 江苏大学硕士学位论文 破,由归纳假设可知石西, 根据限界语义,工罡,西说明 从而耽万?石仍?耽忉?,缈?,即曼,破。 .? ,旃 根据限界语义,。足,确说明存在自然数?七,使得万,卜。?,,由归纳假 设可矢口万萌,‘万?万妒?‘万?,。妒?,即足,磊。 .声岛螽 根据限界语义,。岛西说明对任意的自然数?七,万圳。痧。且路径有循 环点,使得,万朋,由归纳假设可知对任意的自然数?,石训嗔, 耽协?万缈?仞?石卢。办?,因为路径中有循环点,所以它 可以表示无穷路径,所以芝,破 .?罡,稿唬 根据限界语义,卜。 ,萌唬说明存在自然数/?后,使得万/。妒:,且对任 意小于,的自然数,万;矿。,由归纳驾驶可知存在自然数,?,使得万,矿:, 且 , 对 任 意 小 于 的 自 然 数 , , 石圳矽。 ‘石?万缈?‘万?, 女妒?, 即罡,萌欢 .痧罡,磊尺欢 由于妒识尺破兰砍欢旃识,根据前面可知,算子都是满足定理 的,所以算子也是满足定理的。 。最。矽当且仅当 。?.勋??并且前提是蹦 ?鼬矽这里 户女?茁?”?厂?万?万?,?彩?,. .夕最。妒 根据限界语义 。丘。矽说明,?口痧? ?鼢痧芝:??刀?矽 由于万卜。矽蕴含万户矽,所以 ,‰矽,.? ??耽万?万卢? ?,.?‘万?万女?,?勋矽,.? 即 垦。矽概率逻辑的限界模型检测技术 .概率奖励计算树逻辑的限界模型检测算法 本小节我们将探讨如何将%对公式的满足性关系判定问题转换为线 性方程组的求解问题。对于:公式妒,假设对于缈的任意子公式矽,对于 中的每一个状态,我们已经知道是否满足矽。令?为限界模型检测的界,,. ? 为花费边界,,缈,,,.。妒,.。? 。掰,不同的算子对应不同的转 换方法,我们分别讨论,对于原子命题及其否定,以及算子,因它们直观简 单,这里忽略。 .伊磊 当,.或者时,,缈,,,.; 当,.且七?时,,缈,,,.?,’。 ,’?墨 .缈破 当,.时,,缈,,,.; 当,?且时,如果。萌,则,妒,,,,否则,妒,,,; 当,?,.伽且?时,如果。破,则,妒,,,.,否则 讧 ,妒,,。 ,妒,,,.?, ? .妒破 当只有一个状态 当 ?。办 ,妒,,,.; 当。破且,,贝 ,妒,,,.,否贝 ,缈,,,.。 当不只一个状态,令,是路径中的循环点 此时?,当 ?。破或者则,妒,,,.; 当路径片段,?%之间存在状态,使得则,仍惫,,; 当路径片段?之间存在状态,,满足,破则,,缈,’,,’;否则 ,,妙,七’,,.’’,’是任意正整数,缈,,?,’?’,妒,一洲 ? .缈西唬 当,.时,,缈,,,.; 当,.?且时,如果。政,则,妒,,厂,否则,妒,,,.;江苏大学硕士学位论文 当,且七?时,如果。唬,则工,,,,,如果。孬,则 ,?,,,?,’弦’,缈,,; .妒萌触 当时,如果卜。破,则,缈,,,.,否则,缈,,,.; 当膏?时, 故分成两部分: 因为伊萌唬三唬唬萌欢, ,妒,,,.,欢,,,.,识钨人政,因而可以根据前面算子和算子的计 算求得。 .实例:零配置协议 本小节通过一个实例来说明的限界模型检测过程。家庭局部网络与 外面的网络都有一个接口来保持通信。这种 网必须是热插拔的,且自我 配置的。这意味着当一个新的应用连接到网络时,必须给它自动配置唯一的 地址。零配置协议正是为家庭局部网络的应用而设计的,其主要功能是为 新的应用动态配置地址。 零配置协议通过下述方式解决地址的自动配置。首先主机在 个可用的地址中选择一个称为“”,并且发布一条消息称为探针“谁在 使用地址”如果网络中有其它主机正在使用,则其通过消息“我在使用” 作为回应。在收到回应消息后,主机重新配置地址,并重复刚才的过程。因 为消息会丢失或者主机忙,发布的消息可能不能到达某些主机。为了提高协 议的 可靠性,主机需要将同一消息发送门次即要发送门个探针,每一次间隔,个时 间单 位。因此主机在发送完门次消息,并且在门.,个时间单位内没有收到回复的 消息 后,就可以使用选择的地址。但是发送的消息可能会全部丢失,因此执行该协 议 后主机仍然可能会使用正在使用的地址。这种情况称为地址冲突,其会导致 /连接失效。 单个主机试图在网络中配置地址的行为如图.所示:概率逻辑的限界模型检 测技术 图. 零配置协议 将协议的行为用马尔可夫链表示,中有个状态,以表示的是需要的 探针的最大个数上图疗:。假设网络中有个主机,在初始状态&下主机随 机选择一个地址,之后。有两种可能:选择一个了已经使用的地址 的概率为/并且转移到状态蹦选择了一个没有使用的地址的概 率为?并且转移到状态已,。在状态薯?门下主机发送消息探针也有两种可 能:不能得到回应的概率为并且转移到状态。;得到响应的概率为? 并且转移到状态即主机将重新配置选择一个新的地址;在状态下若仍然 没有响应,则转移到状态‖发生地址冲突即主机选择了一个已经被其它主机 使用的地址。这里没有回应包含三种情况:发送的消息丢失、响应的主机忙、 回应的消息丢失。 我们现在分析这个模型中的三个奖励方程: .它表示离开一个状态的等待时间。由于前面说过每次重新发送探针时 都要等待,个时间单位,所以得到每个状态的奖励的值: ,表示主机立即获得一个地址; ,?门表示等待,个时间单位到达下一个状态; 》 ,%,玎.,表示在主机等待了.,个时间单位没有收到响应到达状态 ,说明主机得到了一个没有使用的地址; 。%:,。表示状态没有转移; ? 。瓴。表示在概率非常小的情况下才会发生地址冲突,是一个非 江苏大学硕士学位论文 常大的数。 .它表示离开一个状态所发送的探针数。得到每个状态的奖励的值: ,.%薯?刀表示离开状态发送一个探针; ,门表示发送完疗个探针没有收到响应到达了状态; 其它状态奖励值为。 .它表示为得到一个未使用的地址失败尝试的数目。得到每个状态的奖 励的值: 。表示已经选择了一个正在使用的地址,失败数为; 其它状态奖励值为。 既然已经知道了协议的奖励的方程,下面我们来讨论的限界模型检 测过程。我们分析拘性足?乃。,即主机使用了一个已经被其它主机使用 的地址的概率不低于.。并且考虑,.叫的值。 取,,..,,由的限界模型检测算法可得: ,,,?一。,,,??,,,? ,,,?,,,,?, ,,,?,一?,,,?,?,,,?, ,,,?, ,,,?,一‘,,,?,?,,,?, ,,,,一‘,,,?,?,,,?, ,,,?,,如,,?, ,,,?,一?,,,?,?,,,?, ,,?,,?,一?,,?,,?,?,,,?, ,,,?,一?,确,,?,?,,,?, ,,,?, ,,,?,一?,,,?,?,,,?, ,,,?,一?,,,?,?,,,?, ,,,?,,,,, ,如,,,一?,,,?,?,,,?, ,,,?,一?,,,?,?,,,?, ,,,?,一?,,,,?,,,?, ,,,?,,啊,,, ,,,?,一‘,,,?,?,,,?, ,,,‘一?,,,?,?,,,? ,,,?,一?,,,?,?,,,?, ,,,, ,,,?,一?,,,?,?,,,?, 概率逻辑的限界模型检测技术 ,,,?,,,, ,,,?,一?,,,?,?,,,?, ,,,’一‘,,,?,?,,,?, ,,,?, 氏,,,, ,,,?,一‘,,,?,?,,,?『 ,,,,一。,,,?,?,,,?, ,,,?,,,, ,,,?,一‘,,,,?,,,?, ,,,?,一‘,,,?,?,,,? ,,,?,一。,,,?,?,,,?, ,,,?,一‘,,,?,?,,,?, “黾,取,, ,,,?,一‘,,,?,?,,,?, ,,,, ,,,?,一‘,,,?,?,,,, ,,,?, ,,,?, ,,,?, ,,,?, ,,, ,,,?, ,,,?, ,,,? ,,,?, ,风,,?, 。,,,?, ,,,?, ,,,?, 对于上面的线性方程组,我们用 ..进行求解,求解时我们取 /,., 即 最终得到,,,.,., 。卢:。.。利用文献中介绍的基于不动点的模型检测算法,可以 得到。,。的实际值为.。 接着分析属性丘。?,这里瓯,,同样取七:,计算得 ?君.?,.?’ 而它的实际值利用线性方程组求解得 .?,.?’ 江苏大学硕士学位论文 .测试结果 本小节我们通过三个测试用例来分析限界模型检测算法中模型的边界和线 性方程组未知数个数的关系。 测试用例一:一个简单的模型,如图?所示 , , 图.一个简单的模型 测试的属性为芝??,此时 花费边界,. 路径边界 概率度量 变元个数无边界无边界. 无边界 . . 无边界 . 测试用例二:用硬币模拟掷骰子,如图.所示概率逻辑的限界模型检测技术 图.硬币模拟掷骰子 %为初始状态,目标状态集合,,,,,是骰子可能掷的点数,图中各个 节点表示抛硬币一次,如果硬币为正面则左分支决定下一个状态,如果是反 面则 右分支决定下一个状态。抛硬币结果为正面或反面的概率均为/,此时的奖励 表示抛硬币的次数,除了目标状态所有状态的奖励值为,里面的状态的奖励 值为。测试的属性为 叫:, 花费边界,.