An Isaac Newton Institute Programme

Logic and Algorithms

Model checking for probabilistic real-time systems

17th May 2006

Author: Marta Kwiatkowska (Birmingham)

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. 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 link­local addresses and the FireWire root contention protocol case study.

Related Links