稠密时间区间时序逻辑的可满足性判定  

Decidability of the dense timed interval temporal logic

作　　者：张海宾[1] 段振华[1] 

机构地区：[1]西安电子科技大学计算机学院,陕西西安710071

出　　处：《西安电子科技大学学报》2007年第3期463-467,共5页Journal of Xidian University

基　　金：国家自然科学基金资助项目(60373103);国家自然科学基金重大资助项目(60433010);博士点基金资助项目(20030701015)

摘　　要：定义了稠密时间区间时序逻辑(DTITL),它是区间时序逻辑的一种实时扩充.通过定义DTITL无穷状态空间上的具有有限个数等价类的等价关系,把DTITL的连续状态模型离散化为一阶区间时序逻辑模型.定义了一套规则来构造DTITL公式对应的有界整数域上一阶区间时序逻辑子集SFO的公式,从而把DTITL的可满足性判定问题等价地转化成了SFO的判定问题.利用多个命题变量等价表示有界整数,把SFO的可满足性判定问题等价转换为可判定的命题区间时序逻辑的判定问题.解决了DTITL的可满足性判定问题.We present a dense timed interval temporal logic （DTITL） and exploit the decidability problem of DTITL. To do so, we define an equivalence relation with finite equivalence classes over state spaces of DTITL models. Using the equivalence relation, we can construct a discrete model of a subset of the first order interval temporal logic called SFO from a continuous DTITL model. A set of rules are also applied to construct SFO formulas from DTITL ones. Then the satisfiability of DTITL is equivalently transformed to the same problem for SFO. Since the decidability of SFO can be transformed to the satisfiability of the propositional interval temporal logic, so SFO is decidable. Thus, the satisfiability of DTITL can be proved to be decidable.

关 键 词：实时系统 时序逻辑 模型检查 混合系统 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]