论文部分内容阅读
时序逻辑通常是命题逻辑或谓词逻辑的扩展。时序逻辑的一种重要用途是行为模型的规格说明。时序逻辑的语义决定了一个模型是否满足给定的时序逻辑公式。验证行为模型是否具有给定的时序逻辑性质对有穷状态模型而言可以用算法实现。这类验证方法统称为模型检测。时序逻辑的限界语义的特点是由局部到全局的一种逼近。这种语义为模型检测提供了另一种途径。本报告从理论的角度讨论时序逻辑的限界语义，并介绍基于限界语义的CTL性质的模型检测方法。