基于时间区间时序逻辑的实时系统统一模型检测

Model Checking Real-Time Systems within Unified Approach of Timed Interval Temporal Logic

  • 摘要: 在同一个逻辑框架内无法自动验证实时区间模型的实时区间性质. 为此, 该文使用一个离散时间区间时序逻辑公式建立实时系统模型, 使用另一个离散时间区间时序逻辑公式描述实时系统需要满足的性质, 在此基础上, 离散时间区间时序逻辑统一模型检测问题即可归约为目前已解决的离散时间区间时序逻辑可满足性判定问题. 该文证明了新方法的有效性以及正确性, 为区间实时逻辑这一类的模型检测问题提供了方法.

     

    Abstract: There is no method for model checking real-time systems within the same real-time interval logic. To this end, we restrict a real-time logic, called Timed Interval Temporal Logic (TITL), on discrete time domain. And then, we use a TITL formula to construct an interval model and another TITL formula to describe an interval property. On the basis of this, we formalize a novel approach for model checking within the same logical framework based on TITL. The validity and correctness of the method are proved at last.

     

/

返回文章
返回