[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]
点击复制

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

参考文献/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
Copyright @ 《 智能系统学报》 编辑部
地址:(150001)黑龙江省哈尔滨市南岗区南通大街145-1号楼 电话:0451- 82534001、82518134