ProMoC is a symbolic probabilistic Model Checker. This program uses the OBDD library JINC for the system synthesis and all numerical operations needed to evaluate probabilities. This program was written to examine symbolic methods in the application of Model Checking.
The typical question to ProMoC is:
"With which probability can set T be reached (within less or equal r steps)?"
The set T is specified with CTL. r is defined with the maximum number of rounds. Costs can be assigned to each state through the rewards.
The best way to explain the usage of ProMoC is to look at an example.
We are interested in the question how probable it is to throw two sixes in a row.
The following system models a dice that is thrown till two sixes occur (in a row).
1: const int maxN=2;
2:
3: module dices
4: dice:[1..6] init 1;
5: counter:[0..maxN] init 0;
6:
7: [] (counter<maxN)-> 1/6 :(dice'=1) & (counter'=0)
8: +1/6:(dice'=2) & (counter'=0)
9: +1/6:(dice'=3) & (counter'=0)
10: +1/6:(dice'=4) & (counter'=0)
11: +1/6:(dice'=5) & (counter'=0)
12: +1/6:(dice'=6) & (counter'=counter+1);
13: endmodule
14:
15: rewards
16: true:1;
17: endrewards
The formula counter=2 specifies the set T.
The transition system (without probabilities) is represented in the Figure below.
Every dice throw has cost 1. The maximal number of rounds limits the number of calculation steps. The probabilities for all r (less the maximal number of steps) are represented in the graph and lists in the table. For some systems the calculation of the probabilities can be too time consuming. Therefor ProMoC contains a simulation function. The number of samples can be configured to enhance the accuracy.
For further information please do not hesitate to contact me.