const int k; // step bound // maximum probability robot 1 can guarantee to reach its goal without crashing <>Pmax=? [ !"crash" U "goal1" ] // maximum probability robot 1 can guarantee to reach its goal without crashing within a deadline <>Pmax=? [ !"crash" U<=k "goal1" ] // minimum expected time robot 1 can guarantee to reach its goal <>R{"time1"}min=? [ F "goal1" ]