Model checking for probabilistic real-time systems
Seminar Room 1, Newton Institute
Probabilistic timed automata are timed automata extended with discrete probability distributions, and can be used to model timed randomised protocols or fault-tolerant systems. This talk will give an overview of model-checking algorithms for probabilistic timed automata and their prototype implementations. Firstly, we consider a subclass of probabilistic timed automata and show that the classical approach based on an integral model of time (digital clocks) admits verification of an important class of properties including probabilistic reachability and expected reachability. Next we present a complete symbolic framework for the verification of probabilistic timed automata against the quantitative probabilistic, timed temporal logic PTCTL. The algorithms operate on zones, that is, sets of valuations of the probabilistic timed automaton's clocks, and therefore avoid an explicit construction of the state space. The digital clocks approach enables modelling and quantitative analysis of protocols directly within the probabilistic model checker PRISM (www.cs.bham.ac.uk/~dxp/prism/). The symbolic approach necessitates combining data structures for real-time verification with those for symbolic probabilistic model checking. Both have been applied to analyse performance of real-world randomised protocols such as the dynamic configuration protocol for IPv4 linklocal addresses and the FireWire root contention protocol case study.