Abstract

This is joint work with Gethin Norman, Roberto Segala and Jeremy Sproston.

We consider the timed automata model of Alur and Dill, which allows the analysis of real-time systems expressed in terms of quantitative timing constraints, for example communication protocols, digital circuits with uncertain delay lengths, and media synchronization protocols. Automatic verification of such systems is made possible through a finite-state representation known as a region graph.

Traditional approaches to real-time system description express the model purely in terms of nondeterminism; however, we may wish to express the likelihood of the system making certain transitions. One example could be the probability of a fault occurring in a device, and another the arrival time of a packet on a network being distributed according to some continuous probability distribution.

In this talk we first present a model augmented with discrete probability distributions. Furthermore, using an existing algorithm, we develop a model checking method for such models (which includes fairness) for temporal logic properties which can refer both to timing properties and probabilities, such as, ``with probability 0.6 or greater, the clock x remains below 5 until clock y exceeds 2''.

Finally, we discuss issues that arise when extending the model with continuous time probability distributions, and outline a possible solution.