论文部分内容阅读
定义了稠密时间区间时序逻辑（DTITL），它是区间讨序逻辑的一种实时扩充．通过定义DTITL无穷状态空间上的具有有限个数等价类的等价关系，把DTITL的连续状态模型离散化为一阶区间时序逻辑模型．定义了一套规则来构造DTITL公式对应的有界整数域上一阶区间时序逻辑子集SFO的公式，从而把DTITL的可满足性判定问题等价地转化成了SFO的判定问题．利用多个命题变量等价表示有界整数，把SFO的可满足性判定问题等价转换为可判定的命题区间时序逻辑的判定问题。解决了DTITL的可满足性判定问题。