命题线性时序逻辑的对偶模型问题的复杂性

定义了一个命题线性时序逻辑的对偶模型的概念.一个公式f的对偶模型是指f的满足以下条件的两个模型(即状态的w序列):在每个位置上这两个模型对原子命题的赋值都是对偶的.然后,对于确定一个公式f是否有对偶模型的判定问题(记为DM)和在一个Kripke-结构中确定是否存在从两个给定状态出发的对偶模型满足给定公式f的判定问题(记为KDM)的复杂性进行了研究.证明了以下结果:对于只含有F("Future")算子的命题线性时序逻辑,DM和KDM都是NP完全的;而对于以下命题线性时序逻辑,DM和KDM都是PSPACE完全的:含有F,X ("Next")算子的逻辑、含有U("Until")算子的逻辑、含有U,S,X算子的逻辑以及由Wolper给出的含有正规语言算子的逻辑(一般称为扩展时序逻辑,简称ETL).