论文部分内容阅读
定义了一个命题线性时序逻辑的对偶模型的概念．一个公式厂的对偶模型是指，的满足以下条件的两个模型（即状态的ω序列）：在每个位置上这两个模型对原子命题的赋值都是对偶的．然后，对于确定一个公式，是否有对偶模型的判定问题（记为DM）和在一个Kdpke-结构中确定是否存在从两个给定状态出发的对偶模型满足给定公式，的判定问题（记为KDM）的复杂性进行了研究．证明了以下结果：对于只含有F（“Future”）算子的命题线性时序逻辑，DM和KDM都是NP完全的；而对于以下命题线性时序逻辑，DM和KDM都是PSPACE完全的