时间区间时序逻辑的判定性与表达能力

计算机科学 ›› 2010, Vol. 37 ›› Issue (11): 227-229.

时间区间时序逻辑的判定性与表达能力

朱维军,周清雷

(西安电子科技大学计算机学院西安710071);(郑州大学信息工程学院郑州450052)

出版日期:2018-12-01 发布日期:2018-12-01
基金资助:
本文受国家(863)高技术研究发展计划(No. 2007AA010408)，河南省重大科技攻关计划(No.092101210104)资助。

On the Decidability and Expressive Power of Timed Interval Temporal Logic

ZHU Wei-jun,ZHOU Qing-lei

Online:2018-12-01 Published:2018-12-01

摘要/Abstract

摘要： 模型检测技术在实时系统验证中被广泛使用。离散时间区间时序逻辑满足性是可判定的，因而也是可模型检测的。连续时间域时间区间时序逻辑是否可模型检测，则并不清楚。约束时间域到非负实数，证明了其可满足性是不可判定的，但存在该逻辑的可判定子集，并发现了这样的子集。由于模型检测问题可归约为时序逻辑满足性判定问题，因此结果表明，时间区间时序逻辑不可模型检测，但其可判定子集可模型检测。

关键词: 时间区间时序逻辑，可满足性判定，表达能力，模型检测

Abstract: Model checking is used widely in verification of real-time system. Satisfiability of discrete Timed Interval Temporal Logic is decidable, so is model checking of it, But in dense-time domain, the problem of model checking Timed Interval Temporal Logic is not clear. We prove that Satisfiability of Timed Interval Temporal Logic is un-decidable and we find a subset of Timed Interval Temporal Logic which can be decidable. So, it can be decidable to model checking the subset.

Key words: Timed interval temporal logic, Checking the satisfiability, Expressive power, Model checking

朱维军,周清雷. 时间区间时序逻辑的判定性与表达能力[J]. 计算机科学, 2010, 37(11): 227-229. https://doi.org/

ZHU Wei-jun,ZHOU Qing-lei. On the Decidability and Expressive Power of Timed Interval Temporal Logic[J]. Computer Science, 2010, 37(11): 227-229. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed