www.prismmodelchecker.org

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

Documentation