文件名称：稠密时间区间时序逻辑的可满足性判定 (2007年)
文件大小：166KB
文件格式：PDF
更新时间：2024-06-08 14:32:06
自然科学 论文
定义了稠密时间区间时序逻辑（DTITL），它是区间时序逻辑的一种实时扩充通过定义DTITL无穷状态空间上的具有有限个数等价类的等价关系，把DTITL的连续状态模型离散化为一阶区间时序逻辑模型定义了一套规则来构造DTITL公式对应的有界整数域上一阶区间时序逻辑子集SFO的公式，从而把DTITL的可满足性判定问题等价地转化成了SFO的判定问题利用多个命题变量等价表示有界整数，把SFO的可满足性判定问题等价转换为可判定的命题区间时序逻辑的判定问题解决了DTITL的可满足性判定问题。