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

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.