www.prismmodelchecker.org

PRISM Benchmark Suite - Properties (SMGs)

SMG quantitative reachability

Computing the minimum or maximum probability of reaching some set of states in an SMG, i.e. PRISM properties of the form:

  • <<C>>Pmin=? [ F ... ] or Pmax=? [ F ... ]
  • <<C>>Pmin=? [ ... U ... ] or <<C>>Pmax=? [ ... U ... ]

Quantitative properties only (i.e. the probability is not 0/1 for at least some states).

Model Property PRISM property
& description		 Extra
parameters		 Min/max Notes
avoid exit <<p1>> Pmax=? [ F "at_exit" ]
Maximise the probability of the intruder exiting 		- max
avoid find <<p1>> Pmax=? [ F "found_item" ]
Maximise the probability of the intruder finding the item 		- max
dice p1wins <<p1>> Pmax=? [ F "p1win" ]
Maximise the probability of player 1 winning 		- max
investors greater <<investor1>> Pmax=? [ F ("done1"&v>5) ]
Maximum probability with which investor 1 can guarantee a share value greater than 5 		- max
safe_nav reach <<1>> Pmax=? [ !"crash" U ("robot_goal" | "human_goal" | dl) ]
Maximum probability of reaching the other side without crashing 		- max

SMG qualitative reachability

Checking whether the minimum or maximum probability of reaching some set of states in an SMG is 0 or 1, e.g. PRISM properties of the form:

  • <<C>>P>=1 [ F ... ] or <<C>>P>0 [ F ... ]
Model Property PRISM property
& description		 Extra
parameters		 Min/max Notes
hallway_human save <<p1>> P>=1 [ F "saved" ]
Maximum probability of the agent saving the human is 1 		- max

SMG expected reachability

Computing the minimum or maximum expected accumulated reward/cost to reach some set of states in an SMG, i.e. PRISM properties of the form:

  • <<C>>Rmin=? [ F ... ] or <<C>>Rmax=? [ F ... ]
Model Property PRISM property
& description		 Extra
parameters		 Min/max Notes
task_graph time <<sched>> R{"time"}min=?[ F "tasks_complete" ]
Minimum expected time to complete all tasks 		- min

Benchmarks