Skip to Content


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


const int N;

module workers
  left : [0..N] init N;

  [worker] (left > 0) ->
        0.5: (left' = left - 1)
        + 0.5: true;
  [] (left = 0) -> true;


// see next section
rewards "total_time"
  [] left > 0: 1;

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