**Funded by:**
(grant reference GR/M04617/01)

**Dates:** 1998-2001

Institutions: |
University of Birmingham |

`Model checkers' are software tools which enable automatic checking of systems such as hardware circuits and communication protocols against specifications: when supplied with a description of a system and the intended specification they output `yes' if the specification is satisfied, and `no' otherwise, in which case a counter-example (a trace leading to error) is output as well.

This project is concerned with extending the model checking techniques to the case of randomized distributed algorithms. These are algorithms which are designed to run on hardware consisting of many interconnected processors (and often geographically `distributed', as in the case of a network of processors), and which use randomization, that is, make choices at random, using electronic coin flipping. It turns out that randomized algorithms are much faster than their deterministic counter- parts, but verifying their correctness against the specification is much more involved because of the need for sophisticated probabilistic analysis. Moreover, a model checker may be unable to output `yes' or `no', but instead only the probability of the specification being satisfied.

*Distributed algorithms* are designed to run on
hardware consisting of many interconnected processors.
A *randomized* algorithm contains an assignment
to a variable of an outcome of tossing a fair coin or a
random number generator. Since the seminal paper by
Michael Rabin randomized algorithms have won universal
approval, basically for two reasons: simplicity and speed.
Randomization offers a powerful tool for *symmetry breaking*,
which ensures the existence of solutions to certain network co-ordination
problems, such as distributed consensus, even in the presence of failures.
Randomized distributed algorithms include a number of theoretical
algorithmic schemes, for example the dining philosophers protocol and the consensus
of Aspnes & Herlihy, as well as the practical real-world protocols for Byzantine
agreement due to Kursawe et al and root contention in the IEEE 1394 FireWire.

A necessary consequence of using randomization is the fact that the correctness
statements must combine probabilistic analysis, typically based on some
appropriate probability space on computation paths, with classical, assertion-based reasoning.
Examples include:
"the gas boiler may abort with probability *at most* 0.01",
"termination occurs *with probability* 1", and
"delivery of a video frame is guaranteed within time *t* with probability
*at least* 0.98". The analysis of randomized distributed algorithms becomes very
complex, sometimes leading to errors.

The aim of this project was to *automate*,
all or in part, the verification process for randomized distributed algorithms,
which could be achieved by extending the techniques of
*model checking* to the domain of randomized algorithms.
Model checking, and particularly *symbolic* model checking,
has become an established industry standard
for use in ensuring correctness of systems as well as
exposing flaws in the existing designs,
to mention e.g. tools SMV, SPIN, CWB and FDR, none of which can deal with probability.
At the start of the project, several theoretical model checking algorithms
could be found in the literature, but experimental
work and tool implementation was lagging behind.
In fact, there was only one tool, Probabilistic Verus, which
was capable of
handling probabilistic behaviour, albeit in a limited fashion, but which was
never developed fully to be released for use.

The scientific challenge of the proposal was to firstly identify a suitable representation for randomized distributed algorithms, and then develop appropriate model checking algorithms and efficient data structures which are capable of dealing with the increase in complexity and size of models caused by the need to model distributed computation and include probabilistic behaviour.

- Principal investigator: Marta Kwiatkowska
- Research fellow: Gethin Norman
- Visiting Fellow: Roberto Segala