<p>You may be aware of PRISM, a probabilistic model checker, and <a href="http://www.prismmodelchecker.org/casestudies/" rel="nofollow">PRISM Case Studies</a> which documents (besides others) case studies on the correctness and performance of various <em>randomised distributed algorithms</em> taken from the literature.</p>

<p>It is quite common that one distributed computing problem has several variants (with different assumptions), and each variant has several randomized algorithms. That is, there are quite a few randomized distributed algorithms in the literature.</p>

<p>One way of identifying "new" protocols to check is to pick up an article from the <a href="http://www.prismmodelchecker.org/casestudies/" rel="nofollow">PRISM Case Studies</a>, make a list of randomized algorithms for variants of the problem it is focused on, and choose one algorithm to work with.</p>

CC BY-SA 3.0
2015-05-31T07:05:51.703Z
2015-05-31T07:05:51.703Z
hengxin
<p>I want to model a probabilistic protocol using a model checker, but a lot of protocols are already implemented (e.g. Randomised Dining Philosophers, Dining cryptographers, Synchronous leader election protocol). </p>

<p>Do you know other protocols, similar with aforementioned protocols?</p>

CC BY-SA 3.0
2015-06-02T17:08:20.480Z
I am not an expert in the area, but can you describe the protocol? Does it have a name or is it a variant of a well-known one? Are you using some specific software to model it?
chazisop
<randomized-algorithms><model-checking><markov-chains>
Probabilistic protocols
John Smith
# Probabilistic protocols

(Asked by: username_0 on 2015-05-30)

I want to model a probabilistic protocol using a model checker, but a lot of protocols are already implemented (e.g. Randomised Dining Philosophers, Dining cryptographers, Synchronous leader election protocol).

Do you know other protocols, similar with aforementioned protocols?

**Tags:** randomized-algorithms, model-checking, markov-chains

> **Comments:**
> **username_1**: I am not an expert in the area, but can you describe the protocol? Does it have a name or is it a variant of a well-known one? Are you using some specific software to model it?  

---

## 1 answers

### Answer by username_2 on 2015-05-31. Score: 1 | Accepted answer

You may be aware of PRISM, a probabilistic model checker, and [PRISM Case Studies](http://www.prismmodelchecker.org/casestudies/) which documents (besides others) case studies on the correctness and performance of various *randomised distributed algorithms* taken from the literature.

It is quite common that one distributed computing problem has several variants (with different assumptions), and each variant has several randomized algorithms. That is, there are quite a few randomized distributed algorithms in the literature.

One way of identifying "new" protocols to check is to pick up an article from the [PRISM Case Studies](http://www.prismmodelchecker.org/casestudies/), make a list of randomized algorithms for variants of the problem it is focused on, and choose one algorithm to work with.


---

