FORMATS-FTRTFT 2004 START ConferenceManager    

Symbolic Model Checking for Probabilistic Timed Automata

Marta Kwiatkowska, Gethin Norman, Jeremy Sproston and Fuzhi Wang

Presented at Formal Modelling and Analysis of Timed Systems - Formal Techniques in Real-Time and Fault Tolerant System (FORMATS-FTRTFT 2004), Grenoble, France, September 22-24, 2004


Probabilistic timed automata are an extension of timed automata with discrete probability distributions, and can be used to model timed randomized protocols or fault-tolerant systems. We present symbolic model checking algorithms for verifying probabilistic timed automata against properties of PTCTL (Probabilistic Timed Computation Tree Logic). The algorithms operate on zones, which are sets of valuations of the probabilistic timed automaton's clocks, and therefore avoid an explicit construction of the state space. Furthermore, the algorithms are restricted to system behaviours which guarantee the divergence of time with probability 1. We report on a prototype implementation of the algorithms using Difference Bound Matrices, and present the results of its application to the CSMA/CD and FireWire root contention protocol case studies.

START Conference Manager (V2.47.2)