Verifying Quantitative Properties of Continuous Probabilistic Timed Automata

We consider the problem of automatically verifying realtime systems with continuously distributed random delays. We generalise probabilistic timed automata introduced in Kwiatkowska et al. (1999), an extension of the timed automata model of Alur and Dill (1994), with clock resets made according to continuous probability distributions. Thus, our model exhibits nondeterministic and probabilistic choice, the latter being made according to both discrete and continuous probability distributions. To facilitate algorithmic verification, we modify the standard region graph construction by subdividing the unit intervals in order to approximate the probability to within an interval. We then develop a model checking method for continuous probabilistic timed automata, taking as our specification language Probabilistic Timed Computation Tree Logic (PTCTL). Our method improves on the previously known techniques in that it allows the verification of quantitative probability bounds, as opposed to qualitative properties which can only refer to bounds of probability 0 or 1.