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

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

作　　者：朱创营[1] 常亮[1] 徐周波[1] 李凤英[1] 

机构地区：[1]桂林电子科技大学广西可信软件重点实验室,桂林541004

出　　处：《计算机科学》2013年第10期166-171,共6页Computer Science

基　　金：国家自然科学基金(61363030;61100025;61262030);广西自然科学基金(2012GXNSFBA053169;2012GXNSFAA053220)资助

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

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]