Markov Chains

[Rob Fielding]

I can't envision having state machines without at least having a way to attach transition probabilities. Would it make sense to treat parts without backticks as a "match" that can be annotated with a probability. ie: Just make a proper M/M/1 queue. Or discrete time differential equation. It seems that attaching probabilities for multiple matches, where under 100% match would imply stuttering, but otherwise should do no harm.

lambda := 0.2
mu := 0.3

((x = 0)_{lambda} and (x' = x+1))
or
((x > 0)_{mu} and (x' = x-1))
or
((x > 0)_{lambda} and (x' = x+1))

[Andrew Helwer]

For modeling probability there are three models which are relevant (none of which TLA+ supports):

1. Discrete-Time Markov Chains (DTMCs) where every transition is labeled with a probability and the fan-out probabilities of all transitions from a state must sum to 1; you can ask questions like "what is the probability of reaching this state?" of the model, and it is fairly efficient to convert the DTMC into a matrix and solve for this probability as the solution to a set of linear equations.
2. Markov Decision Processes (MDPs) which mix nondeterminism and probabilistic state transitions; this model is the most similar to TLA+ and if probability were ever to be added to TLA+ this is almost certainly the model that would be used. In this model some (usually most) of the transitions are ordinary nondeterministic transitions as in TLA+, but some states have probabilistic steps fanning out from them. For this model you can ask questions like "what is the maximum or minimum probability of entering this state?". Unfortunately this model is fairly inefficient; roughly speaking how it works is each possible execution trace generates a unique DTMC which the reachability probability needs to be solved for, then the maximum or minimum value is taken over all such DTMCs.
3. Continuous-Time Markov Chains (CTMCs) where instead of each transition being labeled with a probability, it is labeled with a rate denoting the decay of an exponential function controlling how long the system is expected to remain in the source state without taking that transition. Since you seem to be coming from queueing theory this is probably the model you are most familiar with. You can ask questions like "how long do we expect the system to run before reaching this state?" and answering this requires solving some differential equations. Broadly speaking it is more tractable than MDPs and some researchers have used CTMCs to try to approximate MDPs and overcome their limitations.

As said at the start TLA+ does not support any of these models. There is a modeling language which does, called PRISM (http://www.prismmodelchecker.org/). The language is quite rough and is pretty much just a graph/matrix labeling DSL; the entire state space needs to be declared up front.

There is some very basic probability modeling that can be done with TLA+ as demonstrated here: https://github.com/tlaplus/Examples/tree/1f278eacdcf563a303856e82b609129f43923131/specifications/KnuthYao

I wrote a longer blog post talking about the various probabilistic models here: https://ahelwer.ca/post/2020-09-11-probabilistic-distsys/

Andrew Helwer

[Elina Mäkinen]

TLA+ do not have native support for probabilistic analysis. 

If you want more Markov chain analysis consider FizzBee and PRISM. They natively support Markov chain analysis.

PRISM supports DTMC, CTMC and MDP.

FizzBee supports DTMC.  

You can attach both probabilities and rewards/cost for probabilistic and performance analysis. 

--
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 visit https://groups.google.com/d/msgid/tlaplus/31c54ba4-df67-4dfc-b041-15f213f86605n%40googlegroups.com.

[Hillel Wayne]

I really don't like how that FizzBee tutorial spends a bunch of time trash talking PRISM and saying FizzBee is better and easier, but doesn't show any PRISM samples or actually compare the two 

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAHQi85kyExvut7_C_sq1tfEbdyrU%3DLjYzciWtf82MwdEGinsbw%40mail.gmail.com.

[jayaprabhakar k]

Thanks, Hillel, for the feedback! I appreciate it. I didn’t include PRISM examples directly in the docs to avoid redundancy but linked to them where relevant. I also acknowledged PRISM as the state of the art tool for probabilistic modeling. Please let me know if I need to reword anything.

For those unfamiliar, I’m the developer of FizzBee. Here are my thoughts, probabilistic modeling generally involves two phases:

1. Generating the state transition graph
2. Querying the model for statistical properties

FizzBee simplifies the first phase with a Python-like language where you describe the algorithm, and it automatically generates the state graph.
PRISM excels at the second phase with a full pCTL query language. As Andrew and Elina mentioned, PRISM supports DTMC, CTMC, and MDP, while FizzBee currently covers a subset of DTMC with basic scripting for common queries.

Example models in both tools:

PRISM:

• Simulating a single die
• Simulating the sum of two dice (not optimal)
• Optimal model for the sum of two dice

FizzBee:

• Simulating a single die
• Simulating the sum of two dice (not optimal)
• General Knuth-Yao algorithm (including an optimal model for the sum of two dice)

Since this is the TLA+ group, I don’t want to take the thread off course, happy to continue elsewhere if anyone’s interested!

Thanks,

JP

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8sx28qa0DY1nqZ1T7U3dO%2But7w5vTn-PvNbLHkD5BXv81w%40mail.gmail.com.