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

• 作者: 常亮 徐周波 朱创营 李凤英
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 线性时态描述逻辑 模型检测 标记büchi自动机 ALC-类 乘积自动机 判空问题 语义Web
• 年，卷（期）: 2013,（10）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 166-171
• 页数: 6页
• 分类号: TP301
• 字数: 9711字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	常亮	桂林电子科技大学广西可信软件重点实验室	77	450	12.0	17.0
2	李凤英	桂林电子科技大学广西可信软件重点实验室	22	88	5.0	8.0
3	徐周波	桂林电子科技大学广西可信软件重点实验室	53	284	8.0	15.0
4	朱创营	桂林电子科技大学广西可信软件重点实验室	4	17	3.0	4.0