Using formal methods to reason about probabilistic systems

[Andrew Helwer]

A long while back I posted a hilariously uninformed idea about using TLA+ to check systems that use probability: https://groups.google.com/g/tlaplus/c/ZDe9ogog6mE/m/GmBVdr-8DQAJ

After a lot of reading & learning, I've summarized how you actually can do this - not with TLA+ currently, but with PRISM. Includes some very interesting material on the subtle distinction between nondeterminism and probability. Who knows, maybe MDPs could be integrated into TLA+ some day far from now. I hope you enjoy!

https://ahelwer.ca/post/2020-04-15-probabilistic-distsys/

Andrew

[Andrew Helwer]

After reading the Knuth-Yao spec that Ron Pressler & Markus Kuppe wrote (https://github.com/tlaplus/Examples/tree/master/specifications/KnuthYao) I've had some more thoughts on this and think TLA⁺ can be used to analyze probability with addition of some operators built into the model checker.

The basics of how a Markov Decision Process (MDP) works is that some steps are nondeterminism steps and some steps are probabilistic steps. For a given MDP, the main question you want to ask is the minimum or maximum probability of entering a state across all possible paths through the system (asking the exact probability is not a valid question, as different nondeterministic paths can offer different probabilities of entering the same state). Thankfully TLA⁺ is already equipped to make statements about both steps and single states. I imagine this looking as follows:

Next ==

  \/ \E e \in S : Action(e)

ProbabilityMap[e \in S] == 1 / Cardinality(S)

probabilities ==

  /\ [][StepProbability(Action(_), ProbabilityMap)]_vars

probabilistic_safety ==

  /\ ProbabilityLEQ(F, 1/1000)

So StepProbability takes an operator Action as a higher-order parameter, then a ProbabilityMap where elements of DOMAIN ProbabilityMap are fed into Action to create a set of step formulas. ProbabilityMap associates a probability with each step formula, and the sum of these probabilities must be 1.

There would be a set of operators ProbabilityLEQ, ProbabilityLT, ProbabilityGT, and ProbabilityGEQ which work pretty much how you would think. The first parameter is a state formula and the second is a probability. TLC would probably interface with the PRISM modelchecker (which I believe is also written in Java) to check these after the state graph generation step because it requires a totally different type of modelchecking.

Note that the scaling properties of MDP modelchecking are pretty horrifying. Each nondeterministic path through the system is turned into its own Discrete-Time Markov Chain (DTMC), which is a MDP where every step is a probabilistic step. Then reachability probabilities are calculated for each of those (many) DTMCs, and solving reachability probabilities for DTMCs requires setting up a NxN matrix where N is the number of unique states and each element of the matrix is the transition probability between states. These matrices are often sparse, but still - imagine taking the number of states in your model then squaring them! For each path! So it's unclear how much utility there would be to adding this feature to TLA+. One benefit of the clunkiness of languages like PRISM is it makes it difficult to write models that are too large, although I have already managed to do this in my short experience with the language.

Andrew Helwer