Abstractions for probabilistic parameterized systems

Randomized distributed algorithms Since Rabin’s seminal work [Rab83], randomization has emerged as a powerful tool for solving hard problems in distributed computing. Solutions to problems like the Byzantine agreement often rely on mechanisms such as a common random coin toss. The correctness of these randomized algorithms can be formalized by qualitative properties, like “all decided processes agree on the value they have chosen”, or probabilistic wait-free termination, “almost-surely all correct processes choose a value”. The performances of such algorithms are, on the other hand, specified by quantitative properties, like assessing the expected running time, for example, “the mean-time before all processes decide is logarithmic in the number of processes”.

The need for formal verification Most often, only paper-and-pencil proofs of randomized distributed algorithms appear in the literature. However, the combination of distributed aspects and probabilities makes human reasoning difficult. This was already observed by Lehmann and Rabin: “proofs of correctness for probabilistic distributed systems are extremely slippery” [LR81], and it has not changed since [Lam19]. Formal verification techniques can be extremely useful in this context. They would avoid tedious and error-prone manual proofs. Moreover, by increasing confidence in developed algorithms, they would allow for more aggressive optimizations. Parameterized verification of randomized distributed algorithms Reasoning about randomized distributed algorithms requires the development of parameterized verification techniques, where the main parameter is the number of processes. The objective is to demonstrate correctness using any number of processes or to evaluate performance based on the number of processes. number of processes. Past research has suggested modeling formalizms and partial solutions for the parameterized verification of randomized distributed algorithms. For example, see [BKLW21].

Objectives The objective of this thesis is to advance parameterized verification methods for probabilistic distributed systems. Initially, we will focus on algorithms using common random coin. We aim at developing state-space abstractions permitting us to compute approximations of the probability of the specification for all instances, or as a function of the number of participants. The starting point will be to look at abstraction techniques that have been proposed for non-parameterized probabilistic algorithms (see the survey [DGVJ12]) and for parameter-
ized models of non-randomized distributed algorithms (see for instance [ST17, BTW21]). The first objective will be to explore how these independent ideas can be combined and adapted to enable the parameterized verification of models for probabilistic distributed algorithms.