离散时间区间时序逻辑可满足性的判定

On the Decidability of Satisfiability of Discrete TITL Formulae

目前还没有模型检查的方法自动检测模型是否满足时间区间时序逻辑描述的性质.我们约束时间域到离散时间,证明了离散时间区间时序逻辑的可满足性是可判定的,因而是可模型检查的.提出了时间正则图模型,通过从离散时间区间时序逻辑到时间正则图的构造,提出了基于该逻辑的判定算法,该算法可以推广到其它的时序逻辑模型检查,并优于现有的基于自动机的时序逻辑判定方法.

There is no method available for checking whether a model satisfies a property described by a timed interval temporal logic （TITL） formula. In this paper, we formalize a novel model named timed normal form graph （ TNFG ）. In addition, we give a procedure to construct TNFG from discrete TITL formula, and prove that the satisfiability of discrete TITL is decidable. The new method can be also used for other types of temporal logic and it is superior to the existing approaches.