Marta Kwiatkowska (University of Birmingham), Model checking for probabilistic timed automata: Methods, applications and tools

Probabilistic timed automata (PTAs) are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols such as IEEE 1394 (FireWire) root contention, CSMA and IPv4 Zeroconf dynamic link-local addressing. The specification formalism for probabilistic timed automata is PTCTL, a probabilistic variant of Timed CTL, which can express properties such as "what is the minimum probability of 4 video frames being dropped within T seconds?". PTAs and PTCTL can also be extended with a notion of costs, allowing properties such as "what is the maximum expected power consumption during the first 30 seconds?".

Model checking for probabilistic timed automata employs methods from both real-time verification and finite-state probabilistic model checking. The former relies on manipulation of zones, i.e. polyhedra representing constraints on clock values. The latter reduces to the solution of linear optimisation problems. The talk will give an overview of these model checking techniques. We will report on the theoretical results and open problems as well as implementations in the tool PRISM (www.cs.bham.ac.uk/~dxp/prism), and illustrate the results with case studies of randomised protocols.