分支时态描述逻辑ALC-CTL及其可满足性判定

摘要：

时态描述逻辑是将描述逻辑与时态逻辑相结合后得到的逻辑系统,具有较强的描述能力;但是大部分的时态描述逻辑都是将时态算子同时引入到概念和公式中,使得公式可满足性问题的计算复杂度过高.将描述逻辑ALC与分支时态逻辑CTL相结合,提出新的分支时态描述逻辑ALC-CTL.该逻辑没有将时态算子用于概念的构造过程,而是将时态算子引入到公式的构造中;从分支时态逻辑的角度看,相当于将CTL中的原子命题提升为描述逻辑中的个体断言.最终得到的逻辑系统不仅具有较强的刻画能力,还使得公式可满足性问题的复杂度保持在EXPTIME-完全这个级别.通过将CTL的Tableau判定算法与描述逻辑ALC的推理机制有机结合,给出了ALC-CTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性.

关键词：时态描述逻辑、分支时态逻辑、可满足性问题、Tableau算法、复杂度

所属期刊栏目：41

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

资助基金：国家自然科学基金61363030,61100025,61262030;广西自然科学基金2012GXNSFBA053169,2012GXNSFAA053220;广西可信软件重点实验室基金KX201109

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

页数：共7页

页码：205-211