基于标记büchi自动机的时态描述逻辑alc-ltl模型检测

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