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

作者：朱创营; 常亮; 徐周波; 李凤英

来源：计算机科学, 2013, (10): 166-171.

• 线性时态描述逻辑
• 模型检测
• 标记büchi自动机
• ALC-类
• 乘积自动机
• 判空问题
• 语义Web Linear temporal description logic
• Model checking
• Label büchi automation
• ALC-type
• Product automation
• Emptiness problem
• Semantic Web

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

• 单位
  桂林电子科技大学