智能系统学报Issue(6)：714-722,9.DOI:10.3969/j.issn.1673-4785.201303034
含有合取查询的时态描述逻辑ALC-LTL模型检测
Research on the model checking of temporal description logic ALC-LTL with containing conjunctive query
摘要
Abstract
By introducing the description abilities of the description logic ALC into the linear temporal logic LTL, the temporal description logic ALC⁃LTL provides an approach for describing temporal properties of dynamic systems under the semantic Web environment. In this paper, the description ability of ALC⁃LTL is further enhanced by in⁃troducing conjunctive queries into it. Also a temporal description logic model checking algorithm containing con⁃junctive query is proposed, which is composed of three steps. Firstly, all instances satisfying the conjunctive que⁃ries 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 ALC⁃LTL 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 se⁃mantic web service, in the semantic web environment.关键词
线性时态描述逻辑/模型检测/合取查询/语义WebKey words
linear temporal description logic/model checking/conjunctive query/semantic web分类
信息技术与安全科学引用本文复制引用
朱创营,常亮,徐周波,李凤英..含有合取查询的时态描述逻辑ALC-LTL模型检测[J].智能系统学报,2014,(6):714-722,9.基金项目
国家自然科学基金资助项目（61363030，61262030，61100025）；广西自然科学基金资助项目（2012GXNSFBA053169，2012GXNSFAA053220）；广西可信软件重点实验室研究课题资助项目（ KX201109）． （）
