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

Decidability of the dense timed interval temporal logic

定义了稠密时间区间时序逻辑(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.