[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Re: Using formal methods to reason about probabilistic systems
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
On Friday, September 11, 2020 at 12:17:02 PM UTC-4 Andrew Helwer wrote:
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!
Andrew
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/f9123239-83eb-452c-9dd9-9e3aca23ccdcn%40googlegroups.com.