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

作     者：朱创营 常亮 徐周波 李凤英 ZHU Chuangying;CHANG Liang;XU Zhoubo;LI Fengying

作者机构：桂林电子科技大学广西可信软件重点实验室广西桂林541004 

出 版 物：《智能系统学报》 (CAAI Transactions on Intelligent Systems)

年 卷 期：2014年第9卷第6期

页      面：714-722页

核心收录：

学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

主　　题：线性时态描述逻辑 模型检测 合取查询 语义Web 

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