PRISM is a probabilistic specification language. Not only can it tell you whether something in your system is possible, it can also tell you how likely. For example, given
dtmc
const int N;
module workers
left : [0..N] init N;
[worker] (left > 0) ->
0.5: (left' = left - 1)
+ 0.5: true;
[] (left = 0) -> true;
endmodule
// see next section
rewards "total_time"
[] left > 0: 1;
endrewards
The model checker can find the average time it takes to process all N messages with R{"total_time"}=? [ F left=0 ].
Due to inexpressivity issues, I said it wasn’t that useful in Probabilistic Modeling with PRISM, but later came around to it in Two workers are quadratically better than one.
- Related Tags
- Formal Methods