Verifying Quantitative Properties of Continuous Probabilistic Real-Time Automata

Appears: Proceedings of the 11th International Conference on Concurrency Theory (CONCUR '00), State College, PA, USA, LNCS 1877, pages 123-137, August 2000.

Abstract: We consider the problem of automatically verifying real-time systems with continuously distributed random delays. We generalise probabilistic timed automata introduced in [KNSS01], an extension of the timed automata model of [AD94], 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.

Download:
Download the paper from the publisher.

Download an author-created copy of the paper (© Springer-Verlag).