const int k; // step bound used in properties // the probability the robot reaches a goal1 state is at least 0.2 P>=1[ F "goal2" ] // the probability the robot never visits a hazard state is at most 0.1 P<=0.1[ G !"hazard" ] // what is the probability that the robot reaches a state labelled with either goal1 or goal2, while avoiding hazard-labelled states, during the first k steps of operation? P=?[ !"hazard" U<=k ("goal1" | "goal2") ] //the expected number of times the robot visits a hazard labelled state during the first k steps is at most 4.5 R{"r1"}<=4.5 [ C<=k ] // what is the expected number of steps required by the robot before reaching a state labelled goal1 or goal2? R{"r2"}=? [ F ("goal1" | "goal2") ]