| 分支时态描述逻辑ALC-CTL及其可满足性判定 |
| |
| 引用本文： | 李屾,常亮,孟瑜,李凤英. 分支时态描述逻辑ALC-CTL及其可满足性判定[J]. 计算机科学, 2014, 41(3): 205-211 |
| |
| 作者姓名： | 李屾 常亮 孟瑜 李凤英 |
| |
| 作者单位： | 桂林电子科技大学 广西可信软件重点实验室 桂林541004;桂林电子科技大学 广西可信软件重点实验室 桂林541004;桂林电子科技大学 广西可信软件重点实验室 桂林541004;桂林电子科技大学 广西可信软件重点实验室 桂林541004 |
| |
| 基金项目： | 本文受国家自然科学基金(61363030,5,61262030),广西自然科学基金(2012GXNSFBA053169,2012GXNSFAA053220),广西可信软件重点实验室基金(KX201109)资助 |
| |
| 摘 要： | 时态描述逻辑是将描述逻辑与时态逻辑相结合后得到的逻辑系统,具有较强的描述能力;但是大部分的时态描述逻辑都是将时态算子同时引入到概念和公式中,使得公式可满足性问题的计算复杂度过高。将描述逻辑ALC与分支时态逻辑CTL相结合,提出新的分支时态描述逻辑ALC-CTL。该逻辑没有将时态算子用于概念的构造过程,而是将时态算子引入到公式的构造中;从分支时态逻辑的角度看,相当于将CTL中的原子命题提升为描述逻辑中的个体断言。最终得到的逻辑系统不仅具有较强的刻画能力,还使得公式可满足性问题的复杂度保持在EXPTIME-完全这个级别。通过将CTL的Tableau判定算法与描述逻辑ALC的推理机制有机结合,给出了ALC-CTL的Tableau判定算法并证明了算法的可终止性、可靠性和完备性。
|
| 关 键 词： | 时态描述逻辑 分支时态逻辑 可满足性问题 Tableau算法 复杂度 |
| 收稿时间： | 2013-05-03 |
| 修稿时间： | 2013-09-19 |
Branching Temporal Description Logic ALC-CTL and its Satisfiability Decision |
| |
| LI Shen,CHANG Liang,MENG Yu and LI Feng-ying. Branching Temporal Description Logic ALC-CTL and its Satisfiability Decision[J]. Computer Science, 2014, 41(3): 205-211 |
| |
| Authors: | LI Shen CHANG Liang MENG Yu LI Feng-ying |
| |
| Affiliation: | Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin 541004,China;Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin 541004,China;Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin 541004,China;Guangxi Key Laboratory of Trusted Software,Guilin University of Electronic Technology,Guilin 541004,China |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
