基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测

计算机科学 ›› 2013, Vol. 40 ›› Issue (10): 166-171.

基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测

朱创营,常亮,徐周波,李凤英

桂林电子科技大学广西可信软件重点实验室桂林541004;桂林电子科技大学广西可信软件重点实验室桂林541004;桂林电子科技大学广西可信软件重点实验室桂林541004;桂林电子科技大学广西可信软件重点实验室桂林541004

出版日期:2018-11-16 发布日期:2018-11-16
基金资助:
本文受国家自然科学基金(61363030,5,61262030),广西自然科学基金(2012GXNSFBA053169,2GXNSFAA053220)资助

Model Checking of Temporal Description Logic ALC-LTL Based on Label Büchi Automata

ZHU Chuang-ying,CHANG Liang,XU Zhou-bo and LI Feng-ying

Online:2018-11-16 Published:2018-11-16

摘要/Abstract

摘要： 时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中,适合于在语义Web环境下对相关系统的时态性质进行刻画。为了对这些时态性质进行高效的验证,在ALC-LTL的基础上研究了时态描述逻辑的模型检测问题。一方面,使用时态描述逻辑ALC-LTL公式来表示待验证的时态规范；另一方面,在对系统建模时借助描述逻辑ALC对领域知识进行刻画。针对上述扩展后得到的模型检测问题,提出了基于自动机的ALC-LTL模型检测算法。模型检测算法由3个阶段组成:首先将时态规范的否定形式和系统模型分别构造成标记büchi自动机；接下来构造这两个自动机的乘积自动机,并将关于ALC的推理机制融入到乘积自动机的构造过程中；最后对该乘积自动机进行判空检测。与LTL模型检测相比,时态描述逻辑ALC-LTL的模型检测引入了描述逻辑的刻画和推理机制,可以在语义Web环境下对语义Web服务等复杂系统的时态性质进行刻画和验证。

关键词: 线性时态描述逻辑,模型检测,标记büchi自动机,ALC-类,乘积自动机,判空问题,语义Web

Abstract: The temporal description logic introduces the description abilities of the description logic into the proposition temporal logic．It’s suitable for describing the temporal properties of relevant systems under the semantic Web environment．To verify the temporal properties efficiently,the model checking problem of temporal description logic based on ALC-LTL was investigated in this paper．On the one hand,the temporal description logic ALC-LTL formula was used to express the specification to be checked．On the other hand,the description logic ALC was used to model the system which is investigated．For the resulted model checking problems,a model checking algorithm based on label büchi automation was presented．This algorithm composes of three steps．Firstly,the negation of the specification and the model of the system are constructed as two separate label büchi automation,and then constructing a product automation for the two label büchi automations,and the reasoning mechanisms of ALC is embedded in the process of constructing in this step,finally,detecting the emptiness problem for the product automation．Compared with the model checking of propositional temporal logic LTL,the model checking of ALC-LTL is provided with the representation ability and reasoning mechanisms of description logics,and therefore is suitable for the semantic Web environment．

Key words: Linear temporal description logic,Model checking,Label büchi automation,ALC-type,Product automation,Emptiness problem,Semantic Web

朱创营,常亮,徐周波,李凤英. 基于标记Büchi自动机的时态描述逻辑ALC-LTL模型检测[J]. 计算机科学, 2013, 40(10): 166-171. https://doi.org/

ZHU Chuang-ying,CHANG Liang,XU Zhou-bo and LI Feng-ying. Model Checking of Temporal Description Logic ALC-LTL Based on Label Büchi Automata[J]. Computer Science, 2013, 40(10): 166-171. https://doi.org/

参考文献

[1] Clarke E M Jr,Grumberg O,Peled D A．Model Checking [M]．Cambridge,Massachusetts:The MIT Press,1999
[2] van der Hoek W,Wooldridge M．Model checking knowledge and time [C]∥9th Workshop on SPIN(Model Checking Software)．April 2002:25-26
[3] Gammie P,van der Meyden R．Mck:Model checking the logic of knowledge [C]∥International Conference on Computer Aided Verification(CAV’04)．Springer,2004:479-483
[4] 吴立军,苏开乐.多智体系统时态认知规范的模型检测算法[J].软件学报,2004,15(7):1012-1020
[5] Baader F,Calvanese D,McGuinness D,et al.The DescriptionLogic Handbook:Theory,Implementation and Applications [M]．Cambridge:Cambridge University Press,2002
[6] Artale A,Franconi E．A survey of temporal extensions of description logics [J]．Annals of Mathematics and Artificial Intelligence,2000,30(1-4):171-210
[7] Lutz C,Wolter F,Zakharyaschev M．Temporal description logics:a survey[C]∥Demri S,Jensen C S,eds．Proceedings of the 15th International Symposium on Temporal Representation and Reasoning．Los Alamitos:IEEE Computer Society Press,2008:3-14
[8] Baader F,Ghilardi S,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] Katoen J-P．Concepts,Algorithms,and Tools for Model Checking[J]．Arbeitsberichte des Instituts fiir Mathematische Maschinen und Datenevarbeitung,1999,31-32:292
[10] Baader F,Bauer A,Lippmann M．Runtime Verification Using a Temporal Description Logic [C]∥Proceedings of the 7th International Conference on Frontiers of Combining System．2009:149-164
[11] 常亮,王娟,古天龙,等.时态描述逻辑ALC-LTL的Tableau判定算法[J].计算机科学,2011,8(8):150-154
[12] Huang Zhi-sheng,Stuckenschmidt H．Reasoning with Multi-version Ontologies:A Temporal Logic Approach [C]∥Galway,International Semantic Web Conference(ISWC2005)．2005:398-412
[13] Pietro I D,Pagliarecci F,Spalazzi L．Model Checking Semantically Annotated Services [J]．IEEE Transactions on Software Engineering(TSE),2012,38(3):592-608

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed