扩展Tempura语言统一模型检测算法

摘要

In order to find a unified model checking algorithm for extended interval temporal logic (EITL), the de-cidable subset of extended Tempura language, which is an executable subset of EITL, is obtained by defining that the constants and the variables in the first-order extended Tempura are all in a finite enumerable type and by combining the constraint version of the first-order extended Tempura with prepositional EITL. Then, a novel model checking algorithm of EITL in unified logical framework is proposed. The algorithm is used to decide whether a specification program written in the decidable subset of extended Tempura language satisfies the property described as a prepositional EITL formula, and the check includes two steps: to translate the specification program into a prepositional EITL formula and to use the existing EITL satisfiability-checking algorithms to automatically check the property. Case study indicates that the proposed algorithm is effective.%针对扩展区间时序逻辑目前没有可用的统一模型检测算法的问题,找到了该逻辑可执行子集即扩展Tempura语言的可判定子集——首先限定该逻辑一阶部分的常量与变量均为有穷可枚举类型,然后加上该逻辑的命题部分.在此基础上,提出了扩展区间时序逻辑统一模型检测算法,以判定由上述定义的语言子集所书写的规范程序是否满足命题版扩展区间时序逻辑公式所描述的性质.具体方法是首先翻译规范程序到命题扩展区间时序逻辑公式,然后使用该逻辑的公式满足性判定算法进行自动验证.验证实例证实了新方法的有效性.