[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Ideas for model-checking probabilistic consensus systems?

I've continued to look into this topic over the past few months. The greatest barrier is the inaccessibility of the material, which generally assumes too much knowledge of its reader (already knowing what the difference between discrete- & continuous-time markov chains, markov decision problems, and probabilistic timed automata are, for example). I've finally found a resource presenting the material at a level appropriate for general users of TLA+! It's a very readable paper called Model-Checking Meets Probability: A Gentle Introduction [pdf] by a professor named Joost-Pieter Katoen at RWTH Aachen university in Germany.

Basically given a state transition graph (called a Kripke structure in parlance) where each transition has an associated probability, a common question we want to ask is "what is the probability of reaching some set of goal states G where some property is true?" This turns out to have a simple translation to a linear equation Ax=b, where solving for x (using any number of algebraic or numerical methods) gives you the probability of <>G from a set of states. The matrix A encodes transition probabilities between all pairs of states in x, so is enormous, but is generally quite sparse so there are numerous techniques to reduce the memory & processing it requires.

You can express many more advanced questions than <>G (like <>[]G or []<>G or whatever) but it turns out they all reduce to the same algorithm.


On Monday, December 10, 2018 at 1:36:16 PM UTC-8, Andrew Helwer wrote:
I've been toying with spec'ing the snowflake/snowball/avalanche byzantine consensus protocols in TLA+: https://muratbuffalo.blogspot.com/2018/06/snowflake-to-avalanche-novel-metastable.html

These protocols are probabilistic; quoting from Murat's post:

To perform a query, a node picks a small, constant-sized (k) sample of the network uniformly at random, and sends a query message. Upon receiving a query, an uncolored node adopts the color in the query, responds with that color, and initiates its own query, whereas a colored node simply responds with its current color.

The naive way to spec this in TLA+ is as follows:

QuerySample(k) ==
    /\ \E sample \in SUBSET Node :
        /\ Cardinality(sample) = k
        /\ ...

This obviously leads to a HUGE explosion in number of states and all but guarantees infeasibility of model-checking. What other approaches exist for modeling probabilistic properties such as this in TLA+?


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0bf2a3d3-983f-436c-8f33-5c8ed02130ce%40googlegroups.com.