On the Decidability and Expressive Power of Timed Interval Temporal Logic
时间区间时序逻辑的判定性与表达能力

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.