广义可能性计算树逻辑的范式研究

《广义可能性计算树逻辑的范式研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、分类号ＴＰ３０１．２密级公开学号１３２２７５■■■＾ａｒｎｓｕｇａ硕ｉｔ学位论文（学术型）题目广义可能性计算树逻辑的范式研究作者赵杰指导教师李永明教授－级学科名称计算机科学与技术二级学科名称计算机系统结构提交日期二〇—六年五月学位论文原创性声明本人声明所呈交的学位论文是我在导师的指导下进行研巧工作所取巧的研巧成果？尽我所知，除文中己经注明引用的内容和致谢的地方外，本论文不包含其他个人或集体已经发表或揉写过的研巧成果，也不包含本人或他人已申请学位或其他用途

2、使用过的成果？对本文的研巧做出重要贡献的个人和集体，巧已在文中作了明确说明并表示谢意。一本学位论文若有不实或者侵犯他人权利的，本人應意承担切相关的法律责任。扛＞Ｇ？作者ｋ曰期：／（年月＞曰学位论文知识产权及使用授权声明书本人在导师指导下所完成的学位论文及相关成果，知识产权归属陕西师范大学。本人完全了解陕西师范大学有关保存、使用学位论文的规忠允许本论文被査阅和借阅，学校有权保留学位论文并向国家有关部口或机构送交论文的纸质版和电子版，有权将本论文的全部或部分内容编入有关数据库进行检索，可Ｗ采用。本人

3、保证毕业离校后任何复制手段保存和汇编本论文，发表本论文或使用本论文成果时署名单位仍为陕西师范大学？保密论文解密后适用本声明。作者签名：ｆｃ去、日巧：＞。１１年＾月Ｘ日摘要１９８１ａ一自从年Ｃｌｒｋ和Ｅｍｅｒｓｏｎ提出了模型检测，其作为种形式化的自动化验证技术有效的弥补了传统测试方案所遗留的问题，因此受到了人们的普遍的一般过程是这样的关注。模型检测的：首先对需要被检测的系统和被验证的性质进行抽象建模，再通过模型检测算法对模型进行形式化验证来判断系统是否满足对应的性质。，在经典的模型检测理论中，由于无法

4、正确的处理系统的中不确定性问题因一此些学者提出了多种状态迁移的量化扩展，基于广义可能性Ｋｒｉｐｋｅ结构的广一个代表义可能性计算树還辑的模型检测就是其中的。由于时序逻辑的范式在模型检测中有着重要的应用，但是在广义可能性计算树逻辑中还没有对范式进行过系统的研充，因此本文的主要工作就是在此背景下进行的。本文的主要内容如下：１一一正态范式．本文给出了广义可能性计算树逻辑的两种不同的范式ＰｏｓｉｔｉｖｅＮｏｒｍａｌＦｏｒｍ，简记为ＰＮＦ和存在范式ＥｘｉｓｔｅｎｔｉａｌＮｏｒｍａｌＦｏｒｍ，简记为（）（ＥＮ巧，

5、并且给出了对应范式的语构和语义解释。一２．通过归纳假设法证明了对于任意的个广义可能性计算树逻溝的公式都存在与之等价的ＰＮＦ和ＥＮＦ的公式。３一．给出了个将任意的广义可能性计算树逻辑的公式转换为与之对应的ＰＮＦ公式巧ＥＮＦ公式的算法，并且通过实例进行分析说明。，广义可能性，关键词，计算树逻辑范式：模型检测ＩＡｂｓｔｒａｃｔＳｉｎｃｅＣｌａｒｋａｎｄＥｍｅｒｓｏｎｉｎｔｒｏｄｕｃｅｄｔｈｅｎｏｔｏｎｏｆｍｏｄｅｌｃｈｅｃｋｎ１９１ｔｉｉｎｇｉ８ｉ，ｈａｓｂｅｅｎｗｉｄｅｌｙｃｏｎ

6、ｃｅｒｎｅｄｆｏｒｔｈｅｒｅａｓｏｎｔｈａｔｍｏｄｅｌｃｈｅｃｋｉｎｇ，ａｓａｋｉｎｄｏｆｆｏｒｍａｌａ山ｏｍａｔｉｃｖｅｒｉｆｉｃａｔｉｏｎ化ｃｈｎｏｏｃａｎｓｏｌｖｅｔｈｅｒｏｂｅｍｓｌｅｅｒｅｌｇｙ，ｐｌｆｔｏｖｆｒｏｍｔｈｔｒａｄｉｔｉｏｎａｌｌ：ｅｓｔｉｎｍｅｔｈｏｄ．Ｔｈｅｅｎｅｒａｌｓｔｅｓｏｆｍｏｄｅｌｃｈｅｃｋｉｎｉｎｃｌｕｄｅａｂｓｔｒａｃｔｎｇｇｐｇｉｇｔｈｅａｒｏｒｉａｔｅｍｏｄｅｌｏｆ化ｅｃｕｒｒｅｎｔｓｓ化ｍａｎｄｄｅｓｃｒｉ

7、ｂｉｎｔｈｅｖｅｒｉｆｉｅｄｒｏｅｒｔｉｅｓｐｐｐｙｇｐｐ，ｔｈｅｎｄｅｔｅｒｍｉｎｉｎｇｗｈｅｔｈｅｒｔｈｅｓｓｔｅｍｓａｔｉｓｆｉｅｓｔｈｅｒｏｅｒｔｉｅｓｏｒｎｏｔｂｔｈｅｍｅａｎｓｏｆｙｐｐｙｍｏｄｅｌｃｈｅｃｋｉｎａｏｒｔｈｍｓ．ｇｌｇｉＩｎｔｈｅｃｌａｓｓｉｃａｌｔｈｅｏｒｙｏｆｍｏｄｅｌｃｈｅｃｋｉｎｇｔｈｅｒｅａｓｏｎｔｈａｔｔｈｅｕｎｃｅｒｔａｉｎｔ，ｂｙｙｐｒｏｂｌｅｍｓｃａｎｎｏｔｂｅｓｏｌｖｅｄｓｕｃｃｅｓｓｆｕｌｌｙ，ｓｏｍｅ

8、ｓｃｈｏｌａｒｓｐｕｔｆｏｒｗａｒｄｋｉｎｄｓｏｆｕａｎｔｉｔａｔｉｉｖｅｅｘｔｅｎｓｉｏｎｓｏｆ化ｅｔｒａｎｓｉｔｏ打ｓｓｔｅｍｏｎｅｏｆｗｈｉｃｈ