论文摘要：基于可能性测度的计算树逻辑与可能性互模拟

模型检测技术因其具有简洁明了, 自动化程度高等优点, 被应用于工业设计的诸多领域, 特别是硬件系统、软件系统. 这种基于仿真、测试、演绎和推理的自动验证技术作为一种形式化的方法和工具, 可以有效地检测到硬件和软件系统存在的风险和漏洞,这种技术在近二十年得到了极大的发展, 从经典的模型检测到概率模型检测再到如今的可能性测度下的模型检测, 无数的专家和学者对这种形式化的自动验证技术无论是在理论上还是应用上做出了巨大的贡献. 经典的模型检测技术要求系统模型及性质必须是精确无异义的, 然而现实世界无论是从信息的获取还是信息的描述, 往往都具有不确定性, 这种不确定性既包括概率不确定性, 也包括模糊不确定性,2008年, Baier和Katoen以有穷的马尔可夫链(Markov Chain)为概率系统的模型, 建立了基于概率测度的模型检测的原理和方法,这使得模型检测在技术和理论上都极大地提高了一个层面, 也使得模型检测的应用面更加的广泛. 自从Zadeh提出了模糊集的概念后,模糊数学成为数学领域又一个刻画不确定性的经典理论, 而模糊数学最重要的应用领域之一就是计算智能. 因此, 模糊环境下的模型检测技术的研究对于计算机科学理论的发展具有十分重要的意义. 本文即是在这方面的一个尝试, 将可能性测度与模型检测相结合建立了一些基于可能性测度的模型检测的定义和定理等.
在经典模型检测理论中当状态数以指数的形式增加时, 就会发生状态爆炸, 然而在模糊环境下, 由于对状态的刻画模糊化, 所以系统所承受的压力会更大, 同时发生状态爆炸的几率也会增高. 因为互模拟可以有效地化简状态数从而将复杂的分支结构简化, 所以在经典的模型检测技术中, 互模拟作为一种抑制状态爆炸的重要方法. 为了解决可能性测度下的状态爆炸的问题, 可能性测度下互模拟的研究就显得十分的重要.
花费问题在一些分析决策系统中被作为关注的重点. Baier和Katoen又以有穷的马尔可夫链作为概率系统的模型系统地介绍了概率花费的概念, 特别是对于概率可达花费问题作了详细的介绍. 本文则是在可能性测度下作了一些尝试, 初步建立了基于可能性测度的可能性花费的概念, 给出了相关结论.
本文主要工作如下：
(1) 基于可能的Kripke结构, 在计算树逻辑和概率计算树逻辑的基础上提出了基于可能性测度的可能性计算树逻辑(PoCTL*), 可能性计算树逻辑(PoCTL-)的相关概念.
(2) 在经典互模拟和可能性测度的基础上建立了可能性互模拟的相关定义, 给出了对于两个满足可能性互模拟的可能的 Kripke 结构的相互表示以及可能性互模拟的化简.证明了可能性互模拟满足自反性、对称性和传递性, 以及可能性互模拟的迹相等、可能性互模拟闭包事件保可能性等性质.又证明了(PoCTL)等价、(PoCTL*)等价和(PoCTL-)等价与可能性互模拟等价的相互关系.
(3) 对可能性花费问题进行了相关的讨论, 建立了基于可能性测度的可能性花费模型, 可能性花费计算树逻辑(PoRCTL)的语构定义等.

来源：半壳优胜鲸鱼幸运星转载请保留出处和链接！

本文链接：http://87cpy.com/220197.html