[1]朱创营,常亮,徐周波,等.含有合取查询的时态描述逻辑ALC-LTL模型检测[J].智能系统学报,2014,9(6):714-722.[doi:10.3969/j.issn.1673-4785.201303034]
ZHU Chuangying,CHANG Liang,XU Zhoubo,et al.Research on the model checking of temporal description logic ALC-LTL containing conjunctive query[J].CAAI Transactions on Intelligent Systems,2014,9(6):714-722.[doi:10.3969/j.issn.1673-4785.201303034]
点击复制
ZHU Chuangying,CHANG Liang,XU Zhoubo,et al.Research on the model checking of temporal description logic ALC-LTL containing conjunctive query[J].CAAI Transactions on Intelligent Systems,2014,9(6):714-722.[doi:10.3969/j.issn.1673-4785.201303034]
含有合取查询的时态描述逻辑ALC-LTL模型检测
《智能系统学报》[ISSN 1673-4785/CN 23-1538/TP] 卷:
9
期数:
2014年第6期
页码:
714-722
栏目:
学术论文—智能系统
出版日期:
2014-12-25
- Title:
- Research on the model checking of temporal description logic ALC-LTL containing conjunctive query
- 分类号:
- TP301
- 文献标志码:
- A
- 摘要:
- 时态描述逻辑ALC-LTL在命题线性时态逻辑LTL中引入了描述逻辑ALC的刻画能力,可以对语义Web环境下动态系统的时序特征进行刻画。该文在ALC-LTL中进一步引入合取查询,增强ALC-LTL公式的描述能力,并在此基础上给出了含有合取查询的时态描述逻辑模型检测算法。模型检测算法由3个步骤组成:首先,根据时态规范中涉及的合取查询从描述逻辑的角度在系统状态中进行推理和检索,求出满足合取查询的所有实例;其次,将这些实例映射为命题并带入时态规范中,将含有合取查询的ALC-LTL模型检测问题转换为命题LTL的模型检测问题;最后调用LTL的模型检测算法完成规范验证。该工作从描述逻辑的角度对传统的命题线性时态逻辑的模型检测问题进行了扩展,适合于在语义Web环境下对语义Web等动态系统的时态性质进行刻画和验证。
- 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 introducing conjunctive queries into it. Furthermore, 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 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 semantic web service, in the semantic web environment.
- 参考文献/References:
-
[1] Jr CLARKE E M, GRUMBERG O, PELED D A. Model checking[M]. Cambridge: The MIT Press, 1999: 23-28.
[2] Van der HOEK W, WOOLDRIDGE M. Model checking knowledge and time[C]//Model Checking Software. Heidelberg: Springer, 2002: 95-111.
[3] GAMMIE P, Van Der MEYDEN R. Mck: Model checking the logic of knowledge[C]//Computer Aided Verification (CAV’04). Heidelberg: Springer, 2004: 479-483.
[4] 吴立军,苏开乐.多智体系统时态认知规范的模型检测算法[J]. 软件学报, 2004, 15 (7): 1012-1020.WU Lijun, SU Kaile.A model checking algorithm for temporal logics of knowledge in multi-agent systems[J]. Journal of Software, 2004,15(7): 1012-1020.
[5] BAADER F, CALVANESE D, MCGUINNESS D, et al. The description logic handbook: theory, implementation and applications[M]. Cambridge: Cambridge University Press, 2003: 14-18.
[6] ARTALE A, FRANCONI E. A survey of temporal extensions of description logics[J]. Annals of Mathematics and Artificial Intelligence, 2000, 30(1/2/3/4): 171-210.
[7] LUTZ C, WOLTER F, ZAKHARYASCHEV M. Temporal description logics: a survey[C]//Temporal Representation and Reasoning. Los Alamitos: IEEE Computer Society Press, 2008: 3-14.
[8] BAADER F, GHILARDI F, LUTZ C. LTL over description logic axioms[C]//Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning. Cambridge: AAAI Press, 2008: 684-694.
[9] BAADER F, BAUER A, LIPPMANN M. Runtime verification using a temporal description logic[C]//Frontiers of Combining System. Heidelberg: Springer, 2009: 149-164.
[10] 常亮,王娟,古天龙,等.时态描述逻辑ALC-LTL的Tableau判定算法[J]. 计算机科学, 2011, 38(8): 150-154.CHANG Liang, WANG Juan, GU Tianlong, et al. Tableau decision algorithm for the temporal description logic ALC-LTL[J]. Computer Science, 2011, 38(8): 150-154.
[11] ORTIZ M, CALVANESE D, EITER T. Characterizing data complexity for conjunctive query answering in expressive description logics[C]//Proceedings of the 21th AAAI Conference on Artificial Intelligence. London: AAAI Press, 2006: 275-280.
[12] CALVANESE D, De GIACOMO G, LEMBO D, et al. Data complexity of query answering in description logics[J]. Knowledge Representation and Reasoning, 2006(6): 260-270.
[13] HUANG Zhisheng, STUCKENSCHMIDT H. Reasoning with multi-version ontologies: a temporal logic approach[M]//The Semantic Web-ISWC 2005(ISWC2005). Heidelberg: Springer, 2005: 398-412.
[14] 朱创营,常亮,徐周波,等.基于标记büchi自动机时态描述逻辑ALC-LTL模型检测[J]. 计算机科学, 2013, 40(10): 166-171.ZHU Chuangying, CHANG Liang, XU Zhoubo, et al. Model checking of temporal description logic ALC-LTL based on label büchi automata[J]. Computer Science, 2013, 40(10): 166-171.
[15] Di PIETRO I, PAGLIARECCI F, SPALAZZI L. Model checking semantically annotated services[J]//IEEE Transactions on Software Engineering, 2012, 38(3): 592-608.
- 相似文献/References:
-
[1]王晓燕,韩啸,彭君,等.实时并发系统的PTSL模型检测[J].智能系统学报,2017,12(5):694.[doi:10.11992/tis.201706008]
WANG Xiaoyan,HAN Xiao,PENG Jun,et al.PTSL model checking of timed concurrent system[J].CAAI Transactions on Intelligent Systems,2017,12():694.[doi:10.11992/tis.201706008]
备注/Memo
收稿日期:2012-10-1;改回日期:。
基金项目:国家自然科学基金资助项目(61363030,61262030,61100025);广西自然科学基金资助项目(2012GXNSFBA053169, 2012GXNSFAA053220);广西可信软件重点实验室研究课题资助项目(KX201109).
作者简介:朱创营,男,1986年生,博士研究生,主要研究方向为形式化验证、语义Web服务、信息安全;常亮,男,1980年生,教授,博士,主要研究方向为知识表示与推理、形式化方法、智能规划等;徐周波,女,1976年生,副教授,博士,主要研究方向为符号计算、智能规划等。
通讯作者:朱创营.E-mail:39463021@qq.com.
更新日期/Last Update:
2015-06-16