朱维军 ，邓淼磊，周清雷，张海宾

(1. 郑州大学信息工程学院 郑州 450001；2. 西安电子科技大学计算机学院 西安 710071；3. 河南工业大学信息科学与工程学院 郑州 450001)

模型检测技术是近年来研究的热点，已经在硬件与网络协议领域取得了大量的重要应用。其基本思想是，自动验证有穷状态空间是否满足需求的性质，经常采用自动机、Petri网或进程代数建立动态模型，静态性质则使用时序逻辑来表达。普通时序逻辑只能表达孤立点之间的时序性质，而区间时序逻辑(interval temporal logic，ITL)及其规范可执行子集Tempura语言[1]，则可通过chop算子实现对数字电路区间内状态之间以及区间之间时序关系性质的描述。ITL逻辑命题部分PITL公式的可有穷满足的判定算法[2]直到2003年才完成，然而由于非终止并发系统大多具无穷模型，因而很难在该判定算法基础上开发相应的模型检测工具。

针对该问题，扩展区间时序逻辑(extended interval temporal logic，EITL)[3-7]把区间从有穷扩展到无穷，与同类扩展ITL模型至无穷区间[8]相比，前者由于只允许最后区间具无穷模型，因而更适合真实的非终止并发系统。而EITL的规范可执行子集扩展Tempura语言[3,5]更使得规范可以通过执行的方式得到结果。然而，目前EITL满足性判定的方法问题仍未解决，本文对此进行研究。由于一阶部分不可判定，因此只考查命题部分(EPITL)。

1 扩展命题区间时序逻辑EPITL

1.1 语法

1.2 语义

1.3 导出公式

比较EPITL与命题投影时序逻辑(propositional projection temporal logic，PPTL)[9]的语法和语义，不难发现两种区间逻辑的区别：前者拥有两种区间算子chop(即“;”)和chop star(即“ϕ*”)；后者也有两种描述区间语义的算子chop和prj。……