Abstract.
Probabilistic timed automata are timed automata extended with discrete
probability 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 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 probability 1. The paper
presents a symbolic framework for the verification of probabilistic 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.
|