const int k; // step bound

// maximum probability robot 1 can guarantee to reach its goal without crashing
<<robot1>>Pmax=? [ !"crash" U "goal1" ]

// maximum probability robot 1 can guarantee to reach its goal without crashing within a deadline
<<robot1>>Pmax=? [ !"crash" U<=k "goal1" ]

// minimum expected time robot 1 can guarantee to reach its goal
<<robot1>>R{"time1"}min=? [ F "goal1" ]