Getting Started

Get ePMC

To obtain our model checkers, you can either

• Build it yourself following our guide
• Download our pre-built packages

Your first probabilistic model

We introduce a simple probabilistic algorithm by Knuth and Yao [1], which is known as Knuth-Yao die program. The program depicted in the following picture formulates a 6-sided die with a fair coin. The algorithm starts from the step s₀, at every step a coin is tossed and there is 50% chance of taking each of the two possible choices. The algorithm terminates when you reach one of the values for the die on the bottom.

Above procedure can be easily modeled by PRISM language in the following. We only need two variables, namely s and d. The value of s represents that the current state we are at and the value of d indicates the tossed face of the dice we get.

dtmc

module dice

	// local state variable
	s : [0..7] init 0;
	// value of the dice
	d : [0..6] init 0;

	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
	[] s=7 -> (s'=7);

endmodule

Since we have formulated a 6-sided die by a fair coin, what we are going to do next is to prove that the 6-sided die indeed gives us every face with probability 1/6. This property can be expressed by the following PCTL formula:

P=1/6 [F (s=7&d=1)] & P=1/6 [F (s=7&d=2)] & P=1/6 [F (s=7&d=3)] & P=1/6 [F (s=7&d=4)] & P=1/6 [F (s=7&d=5)] & P=1/6 [F (s=7&d=6)]

To verify whether the PCTL holds in the DTMCs, we run EPMC with following command line:

java -jar epmc-standard.jar check --model-input-files dice.prism --property-input-files dice.prop --model-input-type prism --property-input-type prism

As expected, EPMC will report true on this model checking task, which confirms the correctness of the Knuth-Yao die program.

Congratulations !!! You have already completed your first model checking task by EPMC.

Since EPMC supports both PRISM language and JANI specification, we have to specify the input format in the command line explicitly. For more information on how to use EPMC, please read our Tutorials.

Further References

[1] D. Knuth and A. Yao. The complexity of nonuniform random number generation. In Algorithms and Complexity: New Directions and Recent Results, Academic Press. 1976.

[2] The die example. http://www.prismmodelchecker.org/tutorial/die.php. 2017

FAQ