Ideas for model-checking probabilistic consensus systems?

[Andrew Helwer]

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

Andrew

[Leslie Lamport]

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:

   https://lamport.azurewebsites.net/tla/current-tools.pdf

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

   https://lamport.azurewebsites.net/tla/inductive-invariant.pdf

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

Leslie

[Markus Kuppe]

On 10.12.18 15:07, Leslie Lamport wrote:
> I'm not sure if that module is in the current release; you might have
> to download the nightly build to get it.

The 1.5.7 release includes the Randomization module.

Markus

[Andrew Helwer]

Resurrecting this thread, because it continues to recur in my thoughts.

Newcomers to TLA+ are often confused that actions such as a network message getting lost are given the same "weight" as happy path actions like receiving & processing that message. They intuitively think of network failures as a lower-probability event, and want some way to express this. It takes some cajoling to convince them this equal weighting of the unhappy path is actually a good thing - TLA+ requires you to be very explicit about what assumptions are required for your safety or liveness invariants to hold.

But what if we want to address the probabilistic nature of reality head-on? What if we had some way to express safety invariants which only hold probabilistically? How would that work, and what would it look like?

Consider an issue known to any developer in a large company: the flaky unit test. Say you have N unit tests, each with uniform independent probability of failure; if any one of them fails, the whole test run fails. Given probability P of each individual unit test failing, will the test run pass with probability at least 0.5? Let's write this in a spec with some hypothetical extension to the TLA+ language:

--------------------------- MODULE FlakyUnitTests ---------------------------

EXTENDS
    Reals

CONSTANTS
    Test,
    TestFailureProbability

ASSUME
    /\ TestFailureProbability \in {r \in Real : 0 <= r /\ r <= 1}

VARIABLES
    executed,
    succeeded

PTestOutcome[outcome \in BOOLEAN] ==
    IF outcome
    THEN 1 - TestFailureProbability
    ELSE TestFailureProbability

Init ==
    /\ executed = [t \in Test |-> FALSE]
    /\ succeeded = [t \in Test |-> FALSE]

TypeInvariant ==
    /\ executed \in [Test -> BOOLEAN]
    /\ succeeded \in [Test -> BOOLEAN]

SafetyInvariant ==
    /\ (\A t \in Test : executed[t]) =>
        /\ (\A t \in Test : succeeded[t]) WITH P(0.5, 1)

RunTest(t) ==
    /\ ~executed[t]
    /\ \E outcome \in BOOLEAN WITH PTestOutcome:
        /\ succeeded' = [succeeded EXCEPT ![t] = outcome]
    /\ executed' = [executed EXCEPT ![t] = TRUE]

Next ==
    \/ \E t \in Test : RunTest(t)

Spec ==
    /\ Init
    /\ [][Next]_<<executed, succeeded>>

THEOREM Spec => TypeInvariant /\ SafetyInvariant

=============================================================================

Here we use the keyword WITH in two ways:

  1. Expressing the probability of taking each branch in a nondeterministic step

  2. Expressing the probability of a predicate holding true for a state; the P(low, high) function specifies the range in which this probability must lie

If no WITH is specified for a state transition, that state transition is given a 100% probability of occurring.

I want to be clear this isn't a serious language design proposal, but more a sketch of what this capability could look like.

TLC would keep track of two additional float variables for each distinct state: lowest probability, and highest probability. The first is the lowest recorded probability for a sequence of steps to arrive in that state, and the second is the highest recorded probability for a sequence of steps to arrive in that state. These values are updated as additional paths (with corresponding probabilities) are found to each state. The end result is we are able to express probabilistic invariants.

I haven't put a particularly large amount of thought into this, but it does seem like a very neat capability which would enable TLA+ to specify things like the Slush/Snowflake/Snowball/Avalanche protocols, which come with probabilistic guarantees of success analyzed via something called continuous-time Markov chains. So in addition to easily transcribing the pseudocode from the paper to PlusCal, we could also easily transcribe & check the bounds:

Andrew

[k1...@icloud.com]

Rather than waiting for a non-trivial extension to TLA and the toolbox, you may want to explore existing tools that target probabilistic systems, e.g., PRISM. The literature on it should have poiters to formalisms and tools in the area.

[Andrew Helwer]

Per Hillel's post on PRISM (https://www.hillelwayne.com/post/prism/) it doesn't do sets/tuples/etc., you have to hardcode every element in the model; are there other modeling languages which don't have this restriction?

[Hillel Wayne]

I did some research on this and PRISM is actually the most advanced probabilistic modeling language out there. Verifying probability is really, really hard! For your use case you're probs best off writing a python script to autogen PRISM specs for you. You might be able to use the PRISM preprocessor, but that's still in beta: http://www.prismmodelchecker.org/prismpp/

Alernatively you might want to try using one of the experimental extensions to PRISM, like ProFeat: https://wwwtcs.inf.tu-dresden.de/ALGI/PUB/ProFeat/

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6d157040-12c3-491c-94fd-bf1b88c2013e%40googlegroups.com.

[Andrew Helwer]

After talking it out with Hillel this morning I now see probabilistic model checking is waaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaay more difficult than I assumed in my post. For example:

• Every nondeterministic state transition must have a probability associated with it; the only question is whether that probability is uniform
• When there are multiple paths to reach the same state, the probability of reaching that state is the sum of the probabilities of those paths

I had assumed probabilistic model checking looked like basic safety checking, but it looks a lot more similar to liveness checking. Interested in seeing the algorithms behind PRISM and such, though.

Andrew

On Wednesday, August 14, 2019 at 7:41:52 AM UTC-7, Hillel Wayne wrote:

I did some research on this and PRISM is actually the most advanced probabilistic modeling language out there. Verifying probability is really, really hard! For your use case you're probs best off writing a python script to autogen PRISM specs for you. You might be able to use the PRISM preprocessor, but that's still in beta: http://www.prismmodelchecker.org/prismpp/

Alernatively you might want to try using one of the experimental extensions to PRISM, like ProFeat: https://wwwtcs.inf.tu-dresden.de/ALGI/PUB/ProFeat/

On 8/14/19 9:14 AM, Andrew Helwer wrote:

Per Hillel's post on PRISM (https://www.hillelwayne.com/post/prism/) it doesn't do sets/tuples/etc., you have to hardcode every element in the model; are there other modeling languages which don't have this restriction?

On Tuesday, August 13, 2019 at 7:05:18 PM UTC-7, Kai wrote:

Rather than waiting for a non-trivial extension to TLA and the toolbox, you may want to explore existing tools that target probabilistic systems, e.g., PRISM. The literature on it should have poiters to formalisms and tools in the area.

--
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 tla...@googlegroups.com.

[Kai]

If you're prepared to look beyond model checking you could start with McIver & Morgan's monograph. Probabilistic aspects as those described formally in the book become quite important when investigating the presence of covert channels in systems that are meant to protect secrets. There's quite an active area of research around that. You could look for quantitative information flow if you wanted to learn more.

[Andrew Helwer]

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.

Andrew

On Monday, December 10, 2018 at 1:36:16 PM UTC-8, Andrew Helwer wrote: