Sciweavers

CONCUR
2000
Springer

Verifying Quantitative Properties of Continuous Probabilistic Timed Automata

14 years 3 months ago
Verifying Quantitative Properties of Continuous Probabilistic Timed Automata
Abstract. We consider the problem of automatically verifying realtime systems with continuously distributed random delays. We generalise probabilistic timed automata introduced in [19], an extension of the timed automata model of [4], 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
Marta Z. Kwiatkowska, Gethin Norman, Roberto Segal
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 2000
Where CONCUR
Authors Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston
Comments (0)