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

Re: Ideas for model-checking probabilistic consensus systems?

Hi Andrew,

If you're trying to check that the probability of an error is
sufficiently low, you probably want to execute a large number of
simulations and see what percentage of them produce an error.  For
that, see the RandomElement, TLCGet and TLCSet operators defined in
the TLC module that are described here:


The operators defined in the Randomization module might also be
useful; they're described here:


I'm not sure if that module is in the current release; you might have
to download the nightly build to get it.


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