Abstract
Systems analysis is becoming more and more important in different fields such as network applications, communication protocols and client server applications. This importance is seen from the fact that these systems are faced to specific errors like deadlocks and livelocks which may in the major cases cause disasters. In this context, model checking is a promising formal method which permits systems analysis at early stage, thus ensuring prevention from errors occurring. In this paper, we propose an extension of timed temporal logic TCTL with more powerful modalities called TCTLh Delta. This logic permits to combine in the same property clocks quantifiers as well as features for transient states. We formally define the syntax and the semantics of the proposed quantitative logic and we show via examples its expressive power.