概率逻辑的限界模型检测技术分类号.密级坌五. 编号江薄大擎硕士学位论文概率逻辑的限界模型检测技术申请学位级别专业名称亟让篁扭应用撞查论文提交期论文答辩期呈生曼旦至呈生鱼旦皇旦学位授予单位和期江菱太堂 圣生鱼旦答辩委员会主席图美评词人独创性声明本人郑重声明:所呈交的学位论文,是本人在导师的指导下,独立进行研究工作所取得的成果。除文中已注明引用的内容以外,本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体,均己在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。学位论文作者签名:叶萌日期:切年月眵日学位论文版权使用授权书测掣掣弊本学位论文作者完全了解学校有关保留、使用学位论文的规定,同意学校保留并向国家有关部门或机构送交论文的复印件和电子版,允许论文被查阅和借阅。本人授权江苏大学可以将本学位论文的全部内容或部分内容编入有关数据库进行检索,可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。保密 口,在年解密后适用本授权书。本学位论文属于团。不保密学位论文作者签名:叶辐指导教师签名:用彳。年月日如/,年月/多日江苏大学硕士学位论文摘 要模型检测是一种自动化程度非常高的有限状态系统验证技术,目前已经在计算机硬件、通信与安全协议、软件可靠性的验证方面获得了较大的成功。传统模型检测技术关注的是系统行为的绝对正确性,如系统不能进入死锁状态。然而分布式算法,多媒体协议,容错系统等往往关心某种量化属性,如消息传送失败的概率不高于%,在时间内至多个消息丢失的概率不高于.%,请求发送后在个时间单元内得到响应的概率不低于%等等。随机模型检测致力于解决这类属性的自动化验证问题。在随机模型检测中一般使用概率计算树逻辑和连续随机逻辑刻画属性,使用马尔科夫过程,概率时间自动机等建立系统模型。与传统模型检测一样,状态空间爆炸问题也是随机模型检测技术实用化的主要瓶颈。在为缓解状态空间爆炸问题已经提出的诸多理论和方法中,限界模型检测技术是克服状态空间爆炸问题的最为有效的方法之一。本文主要工作是提出了概率奖励计算树逻辑和概率实时认知逻辑的限界模型检测技术,具体包括以下两个方面:.概率奖励计算树逻辑以离散时间马尔可夫链作为系统模型,为缓解该模型上的状态空间爆炸问题,提出了概率奖励计算树逻辑的限界检测技术。首先定义概率奖励计算树逻辑的限界语义,并证明其正确性;其次提出基于线性方程组求解的限界模型检测算法;然后通过实例说明了限界模型检测的过程。最后在概率奖励计算树逻辑的基础上提出了重复可达性和持续性的限界语义和限界模型检测算法,并以实例来说明限界模型检测的过程。实验结果表明在属性成立的证据较短的情况下,限界模型检测能够快速的完成验证。.为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了概率实时认知逻辑。模型检测是验证多智体系统是否满足公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈。为此提出一种的限界模型检测算法。首先,将的模型检测问题转换为无实时算子的的模型检测问题;其次,定义的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界模型检测算法;最后,依据概率度量序列的演化规律和数值计算中牛顿迭代法使用的迭代过程终止判断准则,设计了一系列的限界检测终止性判别准则,并分析了各种准则适用的场景。此外还概率逻辑的限界模型检测技术针对线性方程组的特点,给出了变元求解的次序,从而避免不必要的迭代运算。实例研究表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更少。关键字:模型检测,限界模型检测,概率奖励计算树逻辑,概率实时认知逻辑,状态空间爆炸江苏大学硕士学位论文 , ,. , ., , %. .%.%,. . , . , . , ., ., ,., . ,. ., . . .? ,. .? 概率逻辑的限界模型检测技术 . . .,.,. , ., , , . .:, ,江苏大学硕士学位论文目 录第一章绪论.研究背景?.研究现状?.研究内容及论文组织?。第二章相关的概念.概率分布与度量.离散时间马尔可夫链.概率计算树逻辑?一.马尔可夫链奖励模型?.概率时间自动机?.概率时间自动机的平行组合?.第三章概率奖励计算树逻辑的限界模型检测一.概率奖励计算树逻辑.概率奖励计算树逻辑的语义?一.概率奖励计算树逻辑的等价性?. .概率奖励计算树逻辑的限界语义.概率奖励计算树逻辑的限界模型检测算法.实例:零配置协议?.测试结果?。.重复可达性和持续性.重复可达性和持续性的语义?一.重复可达性和持续性的限界语义. .重复可达性和持续性的限界模型检测算法.实例研究?.本章小结?第四章多智体系统中约简状态空间的限界模型检测算法?一.概率实时解释系统.概率实时认知逻辑.概率实时认知逻辑的语法?.概率实时认知逻辑的语义?.概率知识区域图?.基于概率知识区域图的限界模型检测?.时态逻辑的转换?.的限界模型检测?.的限界模型检测算法?一.线性方程组的求解.实例研究?.火车穿越控制系统一.限界模型检测算法一概率逻辑的限界模型检测技术.终止性选择标准?.本章小结?.第五章结论与展望?.结论.展望参考文献?致谢?.攻读硕士学位期间发表的论文?江苏大学硕士学位论文第一章绪论.研究背景模型检测【自二十世纪八十年代提出以来,已经变成了最成功的自动化验证技术之一。它是一种有限状态系统验证技术,因其自动化程度高,逐渐引起了广泛的关注。目前模型检测被广泛应用于硬件、通信协议、安全协议、分布式算法的正确性证明与可靠性分析,例如 利用模型检测技术成功地验证了微处理器的乱序执行单元【和多处理机的一致性协议【,等验证了/协议和 协议。在模型检测中,系统一般被模型化为一个有穷状态转换系统,如结构、有界网等,检测的属性一般利用时态逻辑公式描述,典型的如计算树时态逻辑【,线性时态逻辑 【。模型检测主要通过遍历有穷状态转换系统的全局空间来验证属性是否成立。模型检测的基本思想是当验证某一系统是否满足属性尸时,把该系统建模成一个相对应的马尔可夫模型。,用逻辑公式。来表示要检测的属性。这样验证系统是否满足属性尸就转化成了验证马尔可夫模型。是否满足逻辑公式矽。的模型检测问题,即 。是否成立。这样就可通过模型检测工具按照特定的模型检测算法对该属性自动验证。常用的模型检测工具有、 、们以及实时模型检测工具、等。若验证系统满足属性时,则会返回真值,若系统不满足属性时,模型检测工具会给出一个不满足该属性的实例,通过对实例的研究来分析属性不成立的原因。计算树逻辑和线性时态逻辑都是属性规范描述语言,利用模型检测算法验证系统是否满足计算树逻辑和线性时态逻辑的属性规范,对确保系统的可靠性具有重要的意义。这两种时态逻辑可以规范系统行为的绝对正确性,如系统运行不可能失败。然而实际生活中有很多随机现象,比如在不可靠信道上传递消息导致的消息丢失,对这一类现象往往更关心某种概率度量,如消息传送失败的概率不高%等等。对这类属性计算树逻辑和线性时态逻辑是无法刻画的,因此研究人员在计算树逻辑和线性时态逻辑的基础上引入了概率算子,得到了概率概率逻辑的限界模型检测技术计算树逻辑】等规约形式,并提出了相应的概率模型检测方法【】 。在概率计算树逻辑中引入奖励算子,得到了概率奖励计算树逻辑】 。实际生活中我们会遇到验证系统的重复可达性和持续性的情况,因此在概率奖励计算树逻辑的基础上进行了修改,得到了概率奖励计算树逻辑的规约形式。知识推理】一直是多个领域的研究人员积极探索的课题,比如哲学、经济、人工智能、分布式系统等。特别是在分布式系统领域,时态认知逻辑【能更准和 提出利用确地描述系统和协议的规范,因此自年模型检测技术完成时态认知逻辑的演绎推理【 】之后,模型检测时态认知逻辑一直是一个重要的研究领域,并且在多智体系统中得到了广泛的应用,例如在文献等将每一个保密家视为一个智体,就餐的多位保密家构成了一中个多智体系统,使用时态认知逻辑刻画了协议的匿名性,利用模型检测技术判断出逻辑公式成立,从而验证了保密家协议的匿名性,在文献中骆翔宇等将铁路控制系统视为一个多智体系统,利用模型检测技术验证了控制系统的活性。模型检测时态认知逻辑的研究主要围绕三个方面进行,包括模型检测算法、系统和属性规范、状态空间约简技术。给定一个系统模型和一个逻辑公式描述的属性规约,检测算法主要判断系统是否满足规约,例如 提出了一种将时态认知逻辑的模型检测问题转化为模型检测问题的方法【。规范主要研究不同特性的逻辑刻画,基本的认知时态逻辑包括】, 然而在实际的应用中,有时必须考虑实时性,比如在火车穿越控制系统中,火车进站的信号发出后安全门必须在秒内关闭等等,为此 等学者提出了实时认知逻辑。在另外一些重要领域,对某些事件发生的可能性进行推理也比较重要,比如“事件发生的概率小于/”, “在请求发出之后两秒内得到响应的概率不低于%”等等。这些规范可以通过在时态认知逻辑中引入表示概率分布的算子得到表示,为此等学者提出了概率认知逻辑, 等提出了概率认知逻辑。本文提出一种概率实时认知逻辑,从而可以对概率、实时以及知识进行推理。模型检测是基于对系统状态空间的穷举搜索,系统的规模随着并发分量的增加,呈指数级增长,因此当一个系统的并发分量较多时,那么状态空间是无限的江苏大学硕士学位论文或是非常大的,这样就可能得不到验证结果或不能在有限时间内得到结果,从而模型检测的执行效率会受到的严重影响。系统的状态空间在并发系统中会随着并发分量的增长而呈指数级别的增加。由于时间连续的属性,在实时系统中会有无数个具体的状态,这将导致状态空间是无限的,这就是所谓的状态空间爆炸问题】 。状态空间爆炸问题是制约模型检测发展应用的一个瓶颈。因此,如何缓解模型检测中状态空间爆炸问题,是充分应用模型检测、提高模型检测效率的关键。与传统的模型检测一样,概率奖励计算树逻辑模型检测和概率实时认知逻辑模型检测也面临着状态空间爆炸问题。因此,如何缓解概率奖励计算树逻辑和概率实时认知逻辑模型检测中的状态空间爆炸问题是需要解决的重要问题,这对于提高这两种逻辑模型检测的效率,使其变得实用性是具有非常重要的理论意义和现实意义。.研究现状多年来许多学者都对状态空间约简技术做了相关的研究,主要包括符号化计算四、抽象【】 、偏序归约、限界检钡等等。年 首次提出将的模型检测问题转换为命题公式的可满足性判定问题【,这被认为是限界模型检测的起源。限界模型检测的基本思想是只遍历足以用来验证某一规范的部分状态空间,优点是不会遇到状态爆炸问题,并且能够快速获取最小长度的反例,内存消耗远小于基于有序二叉决策图的方法,而且无须对变量进行静态或动态排序。年 将限界检测技术应用于的全称片断的验证【年,等进一步提出了多智体系统中验证时态认知逻辑的全称片断的限界模型检测方法【 ,并开发了相应的限界检测工具。等在时态逻辑的语言中引入认知模态词,得到一个新的时态认知。逻辑,并展示了相应的限界模型检测算法【 等将实时性引入到认知逻辑中,得到了一种实时认知逻辑,并提出了的限界模型检测算法【。上述不同逻辑系统的限界检测本质上是为验证的属性寻找反例的过程,并将反例的存在性转换为命题公式的可满足性判定问题。造成能够转换为命题公式可概率逻辑的限界模型检测技术满足性判定问题的关键在于这些反例仅仅涉及状态转换,转换关系可以用命题公式编码。而概率算子的反例由于在路径的转换过程中涉及概率度量,利用命题公式很难进行编码。因此概率算子的限界检测有很多新的特性,这些新特性使得我们必须对概率算子的限界检测进行系统的研究。举例如下,公式尉的证据是一条有穷路径%,.,矗,其中墨满足,因此只需对薯,瓯,之间的转换关系以及吼满足进行编码。而对于