摘要
时态描述逻辑ALC-LTL在命题线性时态逻辑LTL中引入了描述逻辑ALC的刻画能力,可以对语义Web环境下动态系统的时序特征进行刻画。该文在ALC-LTL中进一步引入合取查询,增强ALC-LTL公式的描述能力,并在此基础上给出了含有合取查询的时态描述逻辑模型检测算法。模型检测算法由3个步骤组成:首先,根据时态规范中涉及的合取查询从描述逻辑的角度在系统状态中进行推理和检索,求出满足合取查询的所有实例;其次,将这些实例映射为命题并带入时态规范中,将含有合取查询的ALC-LTL模型检测问题转换为命题LTL的模型检测问题;最后调用LTL的模型检测算法完成规范验证。该工作从描述逻辑的角度对传统的命题线性时态逻辑的模型检测问题进行了扩展,适合于在语义Web环境下对语义Web等动态系统的时态性质进行刻画和验证。
By introducing the description abilities of the description logic ALC into the linear temporal logic LTL, the temporal description logic ALCLTL provides an approach for describing temporal properties of dynamic systems under the semantic Web environment. In this paper, the description ability of ALCLTL is further enhanced by introducing conjunctive queries into it. Also a temporal description logic model checking algorithm containing conjunctive query is proposed, which is composed of three steps. Firstly, all instances satisfying the conjunctive queries occurring in a temporal specification are found out by a regular reasoning mechanism of the description logic ALC. Next, these instances are mapped into propositions according to the specifications′ structure. This allows for the model checking problem of ALCLTL containing conjunctive query to be reduced to the model checking problem of the logic LTL. Finally, the traditional model checking algorithm of LTL is called to finish the rest of the work. The model checking problem of classical propositional linear temporal logic with the description logic is extended. This paper provides an approach for describing and verifying temporal properties of dynamic systems, such as semantic web service, in the semantic web environment.
出处
《智能系统学报》
CSCD
北大核心
2014年第6期714-722,共9页
CAAI Transactions on Intelligent Systems
基金
国家自然科学基金资助项目(61363030
61262030
61100025)
广西自然科学基金资助项目(2012GXNSFBA053169
2012GXNSFAA053220)
广西可信软件重点实验室研究课题资助项目(KX201109)
关键词
线性时态描述逻辑
模型检测
合取查询
语义WEB
linear temporal description logic
model checking
conjunctive query
semantic web
