Verification of Probabilistic Distributed Systems

Nowadays, our interaction with some computer-based devise is unavoidable. We find microprosessors in consumer electronics, means of transport, telecommunication systems, industrial plants, computer networks, medical equipment, etc. The malfunction of any of these systems has a variety of consequences ranging from simply annoyance to life-threatening ones, even deriving on catastrophes. In most of such systems, it is crucial that they provide a correct and efficient service.

Random algorithms, in particular, introduce in many cases faster solutions than traditional algorithms. In many other cases, they even provide solutions otherwise impossible. Of particular interest are concurrent and distributed random algorithms such as protocols like those to select a leader or the ones of Byzantine agreement, where the non-deterministic component interplays with the probabilistic one. The environment of the system or the medium where its components interact also contributes to the randomness behaviour of such system. These cases correspond to situations such as the lost of a message in a network, the faulty behaviour of a component, or the availability of some resource.

The consideration of probabilities within the system behaviour has as a consequence that the properties associated to these systems cannot be interpreted in usual logics. For instance, in this new context, we cannot state program termination as a fact, but instead one can state that "a program terminates with probability 1". Besides, stating sometimes the falsehood of a property is too weak, but stating its validity is impossible. In this sense, a particular example is present in bounded retransmission protocols where it is impossible to state that "every sent message is eventually received". Instead, one could analize the validity of the following so called quantitative property: "every sent message is eventually received with probability 0.99".

The aim of this project is to study and develop techniques and tools for the correctness and performance analysis of concurrent programs with random characteristics.

We focus on the following:

1. the development of techniques and tools for quantitative model checking,
2. the development of techniques based on assertional methods and its implementation using proof checkers, and
3. the development of foundations for systems modeled with continuous probabilities aiming at the future development of analysis techniques and tools.

This project was funded by FONCYT (ANPCyT). It started in 2006 and lasted 3.5 years.