Symbolic Model Checking for Probabilistic Timed Automata?

Probabilistic timed automata are timed automata extended with discrete probabil-ity distributions, and can be used to model timed randomised protocols or fault-tolerant 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 rep-resent sets of valuations of the probabilistic timed automaton’s clocks. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The paper presents a symbolic framework for the verification of prob-abilistic timed automata against the probabilistic, timed temporal logic PTCTL. We also report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies.