作者:雷丽晖; 王静 期刊:《计算机科学》 2018年第04期
分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上...
作者:邓辉 薛艳 李亚利 李永明 期刊:《计算机科学》 2012年第10期
提出了基于可能性测度的计算树逻辑CTL*(PoCTL*)的概念。给出了在可能的Kripke结构中可能性互模拟的定义并对其性质进行了详细的探讨。对商可能性Kripke结构及其相关构造进行了特别的研究。