[1]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]
Copy
Research on the model checking of temporal description logic ALC-LTL containing conjunctive query
CAAI Transactions on Intelligent Systems[ISSN 1673-4785/CN 23-1538/TP] Volume:
9
Number of periods:
2014 6
Page number:
714-722
Column:
学术论文—智能系统
Public date:
2014-12-25
- Title:
- Research on the model checking of temporal description logic ALC-LTL containing conjunctive query
- CLC:
- TP301
- DOI:
- 10.3969/j.issn.1673-4785.201303034
- 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.
- Similar References:
Memo
-
Last Update:
2015-06-16