const int k; // step bound in formula // 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? Pmax=?[ !"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{"moves"}min=? [ F ("goal1" | "goal2") ] // minimum probability the robot can reach a goal2 state Pmin=? [ F "goal2" ] // minimum probability the robot can reach a goal2 state Pmax=? [ F "goal2" ] // minimum probability the robot can reach a goal1 state within k steps Pmin=? [ F<=k "goal2" ] // maximum probability the robot can reach a goal2 state within k steps Pmax=? [ F<=k "goal2" ] // maximum probability the robot never reaches a hazard state Pmax=? [ G !"hazard" ] // maximum probability a goal1 state is reached infinitely often Pmax=? [ G F "goal1" ] // maximum probability the robot never reaches a hazard state and reaches a goal1 state infinitely often Pmax=? [ (G !"hazard")&(G F "goal1") ] // (multi-objective query) pareto curve construction multi(Pmax=? [ G !"hazard" ], Pmax=? [ G F "goal1" ])