Personal tools
You are here: Home Events Abstract Archives 2004 Symbolic Model Checking for Probabilistic Timed Automata

Symbolic Model Checking for Probabilistic Timed Automata

Marta Kwiatkowska Department of Computer Science University of Birmingham 4pm Tuesday 23rd November 2004 Room 2511, JCMB, King's Buildings

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, that is, sets of valuations of the probabilistic timed automaton's clocks, and therefore avoid an explicit construction of the state space. Our method considers only those system behaviours which guarantee the divergence of time with probability 1. The research presented in the talk provides a complete 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.

Joint work with Gethin Norman, Jeremy Sproston and Fuzhi Wang

Document Actions