分划逻辑在线性结构上表达能力的研究

摘要

本文主要研究分划逻辑在线性序结构上的表达能力及其相关性质，主要创造性工作由以下两部分组成：(1) 将确定型自动机和分划逻辑各类型的范式集建立起了联系，类似于的Hintikka 公式通过语法的手法完全刻划模型论中Ehrenfeucht-Fraisse 博弈的语义，这种范式集也是按照一定规则递归生成，通过语法的方式完全刻划有限正则语言的语义背景，然后从有限场合的范式集出发，定义ω字场合的各种范式集，研究这些范式集的表达能力并最终给出刻划ω正则语言的L (P <'1,1> ) 范式集。(2) 分划扩充命题时态逻辑通过加入分划算子P <'1,1> ，增强了经典命题时态逻辑的表达能力。对该扩充逻辑关于stutter 不变性进行了深入研究，给出了其关于stutter 不变性的特征定理，即具备stutter 不变性质的扩充时态逻辑的表达能力和不含○ 算子( 后继Next 算子) 的分划扩充命题时态逻辑相同。这样在具体的模型检测的实现过程中可以看情况地使用偏序归约技术，进而可以大大的减少模型的状态空间数，使相应的模型检测算法效率得到显著提高，使一些状态个数过大的模型检测成为可能。