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

摘要：

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

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

所属期刊栏目：40

分类号：TP301(计算技术、计算机技术)

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

在线出版日期：2013-11-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：166-171