论文部分内容阅读
时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中，适合于在语义Web环境下对相关系统的时态性质进行刻画。为了对这些时态性质进行高效的验证，在ALC-LTL的基础上研究了时态描述逻辑的模型检测问题。一方面，使用时态描述逻辑ALC-LTL公式来表示待验证的时态规范；另一方面，在对系统建模时借助描述逻辑ALC对领域知识进行刻画。针对上述扩展后得到的模型检测问题，提出了基于自动机的ALC-LTL模型检测算法。模型检测算法由3个阶段组成：首先将时态规范的否定形式和系统模型分别构造成标记btichi自动机；接下来