文档介绍：摘要
模型检测是一种被广泛应用的验证有限状态系统性质的自动化验证技术。经过三十多年的研究发展,时态逻辑 LTL 和 CTL 的模型检测问题已经得到了很好的解决。不仅提出了各种高效的实现算法,而且开发了 SPIN、SMV 等多种验证工具予以支撑, 使得该技术在通讯协议验证、计算机系统验证等多领域得到了广泛的应用。
传统的模型检测技术都是基于命题逻辑对系统模型及其性质进行刻画的,然而命题逻辑的描述能力有限,这使得模型检测的应用范围受到限制。时态描述逻辑将描述逻辑的刻画能力引入到命题时态逻辑中,增强了时态逻辑的刻画能力,尤为适用于在语义 Web 环境下对考察对象的时态性质进行刻画。时态描述逻辑的模型检测具有重要的研究意义。
本文以 Franz Baader 等给出的时态描述逻辑 ALC-LTL 为基础,对时态描述逻辑的模型检测问题进行了研究。完成的研究工作主要有:
l 定义了时态描述逻辑 ALC-LTL 的模型检测问题,相应地给出了两个模型检测算法。一方面,在传统的用来构建模型的状态迁移系统中引入了描述逻辑 ALC 知识库,从而可以对所考察的系统的领域知识进行表示;另一方面,使用时态描述逻辑 ALC-LTL 的公式来描述待验证的时态规范。在此基础上, 给出了时态描述逻辑 ALC-LTL 模型检测问题的形式化定义。针对该模型检测问题,分别给出了两个模型检测算法:算法 1 将时态描述逻辑的模型检测问题转换成命题时态逻辑模型检测问题来解决;算法 2 借助标记 büchi 自动机进行检测。
l 在时态描述逻辑 ALC-LTL 中引入合取查询,增强对时态规范的刻画能力;相应地为扩展后的模型检测问题给出了模型检测算法。模型检测算法由三个步骤组成:首先,根据时态规范中涉及的合取查询从描述逻辑的角度在系统状态中进行推理和检索,求出所有满足合取查询的实例;其次,将这些实例映射为命题并带入时态规范中,将 ALC-LTL 的模型检测问题转换为命题 LTL 的模型检测问题;最后调用 LTL 的模型检测算法完成规范验证。
l 对含有合取查询的时态描述逻辑 ALC-LTL 模型检测算法进行优化,给出基于自动机的模型检测算法。算法首先将时态规范的否定形式和系统模型分别构造成标记 büchi 自动机;然后构造这两个自动机的乘积自动机。与通常的乘积自动机构造方式不同,这里的乘积自动机构造是以系统模型状态转移为轴逐步生成乘积自动机的各状态,构造过程中采取措施及时终止不必要的状态生成以降低时间开支。
l 初步研究了时态描述逻辑模型检测问题在语义 Web 服务验证中的应用。与传
统时态逻辑 LTL 的模型检测相比,时态描述逻辑 ALC-LTL 的模型检测引入了描述逻辑的刻画和推理机制,可以在语义 Web 环境下对语义 Web 服务等复杂系统的时态性质进行刻画和验证。
关键词:线性时态描述逻辑;模型检测;标记 büchi 自动机;合取查询;语义 Web
服务。
Abstract
Model checking is an automatic verification technique to verify the properties of the systems with finite states. The problem of the temporal logic LTL and CTL has been essfully solved through 30 years hard work. Not only efficient algorithms of them have been proposed, but also developed a variety of tools such as SPIN and SMV to support. So this technology has been applied widely in many fields such as the verification munication protocol puter system.
The traditional techniques of model checking are based on propositional logic to describe the system’s model and its properties. But the description abilities of the propositional logic limit the application of these techniques at more broad areas. Compared to the propositional logic, the