● 摘要
在实际生活中, 较大的和复杂的系统在运行过程中不可避免地出现不确定的、不一致的信息, 所以经典的模型检测不能处理并发系统中所有的验证问题. 为了处理概率不确定性的系统验证, Baier和Katoen介绍了基于概率测度的模型检测的原理和方法, Hart和Sharir将概率论应用于模型检测. 而现实生活中有很多复杂的问题不满足概率测度下的可加性, 这些问题并不能用概率模型进行验证, 因此对非可加性测度下模型检测的研究具有理论与实际意义. 可能性测度是一种非可加性测度, 基于可能性测度的线性时序逻辑(LTL)和计算树逻辑(CTL)模型检测已经有一些重要的研究成果, 但还有一些重要且关键的问题尚未探讨: 可能性测度下瞬时测度是否存在, 瞬时可能性测度与可达可能性测度的关系, 计算树逻辑和可能性测度下计算树逻辑(PoCTL)的关系等, 本文就针对这几个问题进行探讨.
论文主要做了以下两方面的工作:
(1) 提出了瞬时可能性测度的概念,并用构造法证明了在转移步数限制下的可达可能性测度与可达瞬时可能性测度相等, 受限的转移步数限制下的可达可能性测度与受限可达瞬时可能性测度相等. 探讨了在可能性测度下并、交、补运算成立的条件以及那些LTL性质成立,特别是在强连通子集下重复可达事件和持久性事件的性质.
(2) 基于可能性测度对CTL做了进一步的探讨, 给出了PoCTL公式与CTL公式和PoCTL公式与PoCTL公式分别等价的定义. 利用公式的等价性证明了在非运算下成立. 对PoCTL中事件的可能性大于0以及等于1时的性质做了详细的探讨, 深入研究了PoCTL与CTL的异同, 得出了CTL公式是PoCTL公式的一个真子集. 对CTL公式中的重复事件和持久性事件的定性性质和定量性质进行了详细的研究, 通过例子说明了在可能性测度与概率测度下CTL公式的区别. 最后给出了PoCTL模型检测的步骤和时间复杂度, 说明了模型检测的可行性.