Performance Analysis of Probabilistic Timed Automata using Digital Clocks

Probabilistic timed automata, a variant of timed automata extended with discrete probability distributions, is a modelling formalism suitable for describing formally both nondeterministic and probabilistic aspects of real-time systems, and is amenable to model checking against probabilistic timed temporal logic properties. However, the previously developed verification algorithms either suffer from high complexity, give only approximate results, or are restricted to a limited class of properties. In the case of classical (non-probabilistic) timed automata it has been shown that for a large class of real-time verification problems correctness can be established using an integral model of time (digital clocks) as opposed to a dense model of time. Based on these results we address the question of under what conditions digital clocks are sufficient for the performance analysis of probabilistic timed automata and show that this reduction is possible for an important class of systems and properties including probabilistic reachability and expected reachability. We demonstrate the utility of this approach by applying the method to the performance analysis of three probabilistic real-time protocols: the dynamic configuration protocol for IPv4 link-local addresses, the IEEE 802.11 wireless local area network protocol and the IEEE 1394 FireWire root contention protocol.