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