# 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 Extraparameters Min/max Notes avoid exit <> Pmax=? [ F "at_exit" ] Maximise the probability of the intruder exiting - max avoid find <> Pmax=? [ F "found_item" ] Maximise the probability of the intruder finding the item - max dice p1wins <> Pmax=? [ F "p1win" ] Maximise the probability of player 1 winning - max investors greater <> 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 Extraparameters Min/max Notes hallway_human save <> 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 Extraparameters Min/max Notes task_graph time <> R{"time"}min=?[ F "tasks_complete" ] Minimum expected time to complete all tasks - min