SFM-11:CONNECT: Automated Verification Techniques for Probabilistic Systems

This page provides supplementary material for "Automated Verification Techniques for Probabilistic Systems", a tutorial paper on probabilistic model checking of Markov decision processes (and probabilistic automata), written for the SFM-11:CONNECT summer-school.

Examples

The following PRISM models and command-line instructions illustrate selected examples from the tutorial. Further examples will be added as the functionality becomes available in PRISM.
• Example 4 (p.13): running-fig2.nm
`prism running-fig2.nm -pctl 'Pmin=? [ F s=2 ]' -v`
• Example 5 (p.14): running-fig2.nm
`prism running-fig2.nm -pctl 'Pmax=? [ F s=3 ]' -v`
• Example 6 (p.15): running-fig5.nm
`prism running-fig5.nm -pctl 'Pmax=? [ F s=2 ]' -epsilon 0.001 -v`
• Example 7 (p.17): running-ex7.nm
`prism running-ex7.nm -pctl 'Pmax=? [ F s=2 ]' -politer -nopre -v`
• Section 5.1 (p.21): rewards-fig6.nm
`prism rewards-fig6.nm -pctl 'Rmax=? [ I=3 ]' -s -v`
• Example 8 (p.21): running-fig2.nm
`prism running-fig2.nm -pctl 'const int k; Rmax=? [ I=k ]' -const k=4 -s -v`
• Section 5.2 (p.22): rewards-fig6.nm
`prism rewards-fig6.nm -pctl 'Rmin=? [ C<=3 ]' -s -v`
• Example 9 (p.22): running-fig2.nm
`prism running-fig2.nm -pctl 'const int k; Rmax=? [ C<=k ]' -const k=4 -s -v`
• Example 10 (p.24): running-fig5.nm
`prism running-fig5.nm -pctl 'Rmin=? [ F (s=2|s=3) ]' -s -v`
• Example 11 (p.29): running-fig2.nm
`prism running-fig2.nm -pctl 'P<1 [ X (P>=0.5 [ !"fail" U "initial" ]) ]' -v`
• Example 13 (p.34): safety-fig9.nm
`prism safety-fig9.nm -pctl '1 - Pmax=? [ F "A_A_err_acc" ]' -v`
• Example 15 (p.36): running-ltl.nm
`prism running-ltl.nm -pctl 'Pmax=? [ (F G !"L1") & (G F "K1") ]' -v`
• Example 16 (p.38): running-ltl2.nm
`prism running-ltl2.nm -pctl 'Pmax=? [ (F G !"L1") & (G F "K1") ]' -v`
• Example 17 (p.42): multiprod-fig15.nm
`prism multiprod-fig15.nm -pctl 'multi(P>=0.6 [ F "T1" ], P>=0.3 [ F "T2" ])' -lp -v`

Case Studies

Below are PRISM files for the three case studies described in Section 10.

• Israeli and Jalfon’s Self-stabilisation Protocol
• Dynamic Power Management
• Aspnes & Herlihy’s Consensus Algorithm