首页--工业技术论文--自动化技术、计算机技术论文--计算技术、计算机技术论文--一般性问题论文--理论、方法论文

基于广义可能性测度的互模拟及CTL不动点语义

摘要第3-4页
Abstract第4-5页
第1章 前言第8-10页
    1.1 模型检测的研究背景第8-9页
    1.2 基于测度理论的模型检测研究现状第9页
    1.3 本文主要内容第9-10页
第2章 预备知识第10-16页
    2.1 经典模型检测理论基础第10-13页
        2.1.1 经典Kripke结构第10-11页
        2.1.2 经典计算树逻辑第11-13页
    2.2 经典互模拟第13-14页
    2.3 经典不动点理论第14-16页
第3章 广义可能性计算树逻辑第16-22页
    3.1 广义可能性Kripke结构第16-18页
        3.1.1 GPKS的定义第16-17页
        3.1.2 广义可能性测度第17-18页
    3.2 广义可能性计算树逻辑第18-22页
        3.2.1 GPoCTL的语法第18-19页
        3.2.2 GPoCTL~*、GPoCTL~-及GPoRCTL的语法第19-22页
第4章 广义可能性互模拟第22-28页
    4.1 广义可能性互模拟第22-24页
        4.1.1 广义可能性互模拟的定义第22-23页
        4.1.2 广义可能性互模拟的相关概念第23-24页
    4.2 广义可能性互模拟的逻辑刻画第24-28页
        4.2.1 广义可能性互模拟状态与GPoCTL、GPoCTL~*和GPoCTL~-公式的等价性第24-27页
        4.2.2 互模拟等价定理的应用第27-28页
第5章 广义可能性计算树逻辑的不动点语义第28-38页
    5.1 GPoCTL的不动点语义形式第28-33页
    5.2 不动点算法及其复杂度分析第33-34页
    5.3 利用不动点算法验证恒温器性质第34-38页
结论第38-40页
参考文献第40-44页
致谢第44-46页
攻读硕士学位期间科研成果第46页

论文共46页,点击 下载论文
上一篇:一种基于地域划分的个性化推荐算法
下一篇:异构数据流下基于地理位置的时间线研究