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.