含有合取查询的时态描述逻辑ALC-LTL模型检测

• 作者: 常亮 徐周波 朱创营 李凤英
• 来源期刊: 智能系统学报
• 学科: 工学
• 关键词: 线性时态描述逻辑 模型检测 合取查询 语义Web
• 年，卷（期）: 2014,（6）
• 页码范围: 714-722
• 页数: 9页
• 分类号: TP301
• 字数: 10713字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-4785.201303034

摘要

时态描述逻辑ALC?LTL在命题线性时态逻辑LTL中引入了描述逻辑ALC的刻画能力，可以对语义Web环境下动态系统的时序特征进行刻画。该文在ALC?LTL中进一步引入合取查询，增强ALC?LTL公式的描述能力，并在此基础上给出了含有合取查询的时态描述逻辑模型检测算法。模型检测算法由3个步骤组成：首先，根据时态规范中涉及的合取查询从描述逻辑的角度在系统状态中进行推理和检索，求出满足合取查询的所有实例；其次，将这些实例映射为命题并带入时态规范中，将含有合取查询的ALC?LTL模型检测问题转换为命题LTL的模型检测问题；最后调用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