● 摘要
自H. Hansson在20世纪90年代提出概率测度和有穷马尔可夫链的概率计算树逻辑的理论之后, C. Baier对其进行了深入的研究, 并对概率互模拟事件的封闭性和马尔可夫决策过程中事件的可达性进行了详细分析. 但是在现实生活中存在着许多模糊的不确定的事件, 这些事件中蕴含着诸多模糊的属性, 比如概念的不准确等等, 以致基于概率测度的模型检测无法解决. 因此, 基于可能性测度的计算树逻辑、互模拟以及可能的Kripke结构决策过程的研究就显得非常重要, 本文就上述问题进行了较为详细的探讨和研究.
本文主要做了以下工作:
(1) 提出了可能的Kripke结构, 构建了基于可能的Kripke结构的可能性测度, 定义了可能性计算树逻辑PoCTL的语构及语义, 验证了某些PoCTL和CTL公式的等价性, 并证明了不能由CTL表达的事件eventually always a, 可以由PoCTL描述.
(2) 提出了可能的互模拟等相关概念, 给出了状态和路径的互摸拟等价, 及可能的Kripke结构商的定义, 建立了互模拟封闭的sigma-代数. 证明了从两个互摸拟等价的状态出发的路径, 其转移的可能性相等. 给出了PoCTL*和PoCTL—公式, 详细讨论了两个互摸拟等价的状态满足相同的PoCTL、PoCTL*和PoCTL—公式.
(3) 给出了可能的Kripke结构决策过程及调度表的概念, 对可能的Kripke结构决策过程是否有与之相对应的可能的Kripke结构进行了讨论. 给出了定量的PoCTL在可能的Kripke结构决策过程下的语构和语义, 验证了在可能的Kripke结构决策过程下等价的PoCTL公式在可能的Kripke结构下依然等价. 对可能的Kripke结构决策过程中事件的可达性进行了详细讨论, 并给出了一个基于值迭代的算法, 用于计算可达事件的可能性.
相关内容
相关标签