Verifying Quantitative Properties of Continuous Probabilistic Real-Time Graphs

We consider the problem of automatically verifying real-time systems with continuously distributed random delays. Our system model is an extension of the timed automata variant of [15], and exhibits nondeterministic and probabilistic choice, the latter being made according to both discrete distributions and continuous density functions with finite support. To facilitate algorithmic verification, we modify the standard region graph construction by subdividing certain unit intervals in order to approximate the probability to within an interval. Using results of [3, 15] we then develop a model checking method for such systems, 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