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

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