分划扩充命题时态逻辑关于stutter不变性的特征定理

A Stutter-Invariant Characterization for Partition Extended PTL

分划扩充命题时态逻辑通过加入分划算子P^(1,2),增强了经典命题时态逻辑的表达能力。本文就该扩充逻辑关于stutter不变性的研究,给出了它的一个关于stutter不变性的特征定理,即具备stutter不变性质的扩充时态逻辑的表达能力和不含○算子(后继Next算子)的分划扩充命题时态逻辑相同。这样在具体的模型检测的实现过程中可以看情况地使用偏序归约技术,进而可以大大地减少模型的状态空间数,使相应的模型检测算法效率得到显著提高,使一些状态个数过大的模型检测成为可能。

We give a stutter-invariant characterization theorem of partition extended PTL. The main result is that stutter-invariant properties are expressible without next operator. In application, we can associate this result with partial order reduction technique to greatly reduce state space in model checking algorithm and make the latter sub- stantially more efficient.