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

• Type: Conference
• Year: 2004
• Where: FORMATS
• Authors: Marta Z. Kwiatkowska, Gethin Norman, Jeremy Sproston, Fuzhi Wang
• Keywords: FORMATS 2004, Probabilistic Timed Automata, Probabilistic Timed Automaton, Timed Randomised Protocols