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:
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