Temporal logics for the specification of performance and reliability

In this paper we present a methodology for the verification of performance and reliability properties of discrete real-time systems. The methodology relies on a temporal logic that can express bounds on the probability of events and on the average time between them. The semantics of the logics is defined with respect to timed systems that exhibit both probabilistic and nondeterministic behavior. We present model-checking algorithms for the algorithmic verification of the specifications, and we discuss their complexity.