Sciweavers

FORMATS
2004
Springer

Symbolic Model Checking for Probabilistic Timed Automata

13 years 9 months ago
Symbolic Model Checking for Probabilistic Timed Automata
Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or faulttolerant systems. We present symbolic model-checking algorithms for probabilistic timed automata to verify both qualitative temporal logic properties, corresponding to satisfaction with probability 0 or 1, and quantitative properties, corresponding to satisfaction with arbitrary probability. The algorithms operate on zones, which represent sets of valuations of the probabilistic timed automaton’s clocks. Our method considers only those system behaviours which guarantee the divergence of time with
Marta Z. Kwiatkowska, Gethin Norman, Jeremy Sprost
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where FORMATS
Authors Marta Z. Kwiatkowska, Gethin Norman, Jeremy Sproston, Fuzhi Wang
Comments (0)