资源描述：
《概率逻辑的限界模型检测技术》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、概率逻辑的限界模型检测技术分类号.密级坌五.编号⑨江薄大擎硕士学位论文概率逻辑的限界模型检测技术申请学位级别专业名称亟±让篁扭应用撞查论文提交期论文答辩期呈生曼旦至呈生鱼旦皇旦学位授予单位和期江菱太堂圣生鱼旦答辩委员会主席图美评词人独创性声明本人郑重声明:所呈交的学位论文,是本人在导师的指导下,独立进行研究工作所取得的成果。除文中已注明引用的内容以外,本论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本文的研究做出重要贡献的个人和集体,均己在文中以明确方式标明。本人完全意识到本声明的法律结果由本人承担。学位论
2、文作者签名:叶萌日期:切’年‘月眵日学位论文版权使用授权书测掣掣弊本学位论文作者完全了解学校有关保留、使用学位论文的规定,同意学校保留并向国家有关部门或机构送交论文的复印件和电子版,允许论文被查阅和借阅。本人授权江苏大学可以将本学位论文的全部内容或部分内容编入有关数据库进行检索,可以采用影印、缩印或扫描等复制手段保存和汇编本学位论文。保密口,在年解密后适用本授权书。本学位论文属于团。不保密学位论文作者签名:叶辐指导教师签名:用‖彳。年月日如/,年‖月/多日江苏大学硕士学位论文摘要模型检测是一种自动化程度非常高的有限状态
3、系统验证技术,目前已经在计算机硬件、通信与安全协议、软件可靠性的验证方面获得了较大的成功。传统模型检测技术关注的是系统行为的绝对正确性,如系统不能进入死锁状态。然而分布式算法,多媒体协议,容错系统等往往关心某种量化属性,如消息传送失败的概率不高于%,在时间内至多个消息丢失的概率不高于.%,请求发送后在个时间单元内得到响应的概率不低于%等等。随机模型检测致力于解决这类属性的自动化验证问题。在随机模型检测中一般使用概率计算树逻辑和连续随机逻辑刻画属性,使用马尔科夫过程,概率时间自动机等建立系统模型。与传统模型检测一样,状态
4、空间爆炸问题也是随机模型检测技术实用化的主要瓶颈。在为缓解状态空间爆炸问题已经提出的诸多理论和方法中,限界模型检测技术是克服状态空间爆炸问题的最为有效的方法之一。本文主要工作是提出了概率奖励计算树逻辑和概率实时认知逻辑的限界模型检测技术,具体包括以下两个方面:.概率奖励计算树逻辑以离散时间马尔可夫链作为系统模型,为缓解该模型上的状态空间爆炸问题,提出了概率奖励计算树逻辑的限界检测技术。首先定义概率奖励计算树逻辑的限界语义,并证明其正确性;其次提出基于线性方程组求解的限界模型检测算法;然后通过实例说明了限界模型检测的过程
5、。最后在概率奖励计算树逻辑的基础上提出了重复可达性和持续性的限界语义和限界模型检测算法,并以实例来说明限界模型检测的过程。实验结果表明在属性成立的证据较短的情况下,限界模型检测能够快速的完成验证。.为了形式化描述多智体系统中与概率、实时、知识相关的性质,提出了概率实时认知逻辑。模型检测是验证多智体系统是否满足公式的主要技术,状态空间爆炸是该技术实用化的主要瓶颈。为此提出一种的限界模型检测算法。首先,将的模型检测问题转换为无实时算子的的模型检测问题;其次,定义的限界语义,并证明其正确性;然后,设计基于线性方程组求解的限界
6、模型检测算法;最后,依据概率度量序列的演化规律和数值计算中牛顿迭代法使用的迭代过程终止判断准则,设计了一系列的限界检测终止性判别准则,并分析了各种准则适用的场景。此外还概率逻辑的限界模型检测技术针对线性方程组的特点,给出了变元求解的次序,从而避免不必要的迭代运算。实例研究表明,与无界模型检测相比,在属性为真的证据较短的情况下,限界模型检测完成验证所需空间更少。关键字:模型检测,限界模型检测,概率奖励计算树逻辑,概率实时认知逻辑,状态空间爆炸江苏大学硕士学位论文,,,.,.,,,,%..%.%,..,,.,.,.....
7、,.,,.,.,..,....?,..?概率逻辑的限界模型检测技术...,.,.,.,,,,..:,,,,江苏大学硕士学位论文目录第一章绪论.研究背景?...研究现状?...研究内容及论文组织??。第二章相关的概念.概率分布与度量.离散时间马尔可夫链.概率计算树逻辑?一.马尔可夫链奖励模型??...概率时间自动机?..概率时间自动机的平行组合??.第三章概率奖励计算树逻辑的限界模型检测一.概率奖励计算树逻辑..概率奖励计算树逻辑的语义??一..概率奖励计算树逻辑的等价性?...概率奖励计算树逻辑的限界语义.概率奖励计算
8、树逻辑的限界模型检测算法.实例:零配置协议?.测试结果?。.重复可达性和持续性..重复可达性和持续性的语义??一..重复可达性和持续性的限界语义....重复可达性和持续性的限界模型检测算法..实例研究?...本章小结?第四章多智体系统中约简状态空间的限界模型检测算法?一.概率实时解释系统..概率实时认知逻辑..概率实时认知逻辑的语
