A framework for reasoning about time and reliability

A logic is presented for stating properties such as `after a request for service there is at least a 98% probability that the service will be carried out within 2 s´. The logic extends the temporal logic CTL by E.A. Emerson et al. (1983) with time and probabilities. Formulas are interpreted over discrete time Markov chains. Algorithms are provided for checking that a given Markov chain satisfies a formula in the logic. An example is included to illustrate the algorithms