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

Ideas for model-checking probabilistic consensus systems?

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+?