含有合取查询的时态描述逻辑ALC-LTL模型检测

摘要：

时态描述逻辑ALC?LTL在命题线性时态逻辑LTL中引入了描述逻辑ALC的刻画能力，可以对语义Web环境下动态系统的时序特征进行刻画。该文在ALC?LTL中进一步引入合取查询，增强ALC?LTL公式的描述能力，并在此基础上给出了含有合取查询的时态描述逻辑模型检测算法。模型检测算法由3个步骤组成：首先，根据时态规范中涉及的合取查询从描述逻辑的角度在系统状态中进行推理和检索，求出满足合取查询的所有实例；其次，将这些实例映射为命题并带入时态规范中，将含有合取查询的ALC?LTL模型检测问题转换为命题LTL的模型检测问题；最后调用LTL的模型检测算法完成规范验证。该工作从描述逻辑的角度对传统的命题线性时态逻辑的模型检测问题进行了扩展，适合于在语义Web环境下对语义Web等动态系统的时态性质进行刻画和验证。

关键词：线性时态描述逻辑、模型检测、合取查询、语义Web

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

资助基金：国家自然科学基金资助项目61363030，61262030，61100025；广西自然科学基金资助项目2012GXNSFBA053169，2012GXNSFAA053220；广西可信软件重点实验室研究课题资助项目 KX201109．

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

页数：共9页

页码：714-722