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

摘要：

定义了一个命题线性时序逻辑的对偶模型的概念.一个公式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).

关键词：命题线性时序逻辑、对偶模型、计算复杂性

所属期刊栏目：18

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金60223005;60573012;国家重点基础研究发展计划973计划2002cb312200

在线出版日期：2007-08-06（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：1573-1581