const int k; // step bound // robots try to maximise the probability of reaching their goals without crashing <>max=? (P[ !"crash" U "goal1" ] + P[ !"crash" U "goal2" ]) // robots try to maximise the probability of reaching their goals without crashing within a bounded number of steps <>max=? (P[ !"crash" U<=k "goal1"] + P[ !"crash" U<=k "goal2"]) // robots try to maximise the probability of reaching their goals without crashing // where the first one only has a bounded number of steps to do so <>max=? (P[!"crash" U<=k "goal1"] + P[!"crash" U "goal2"]) // robots try to minimise the expected time to reach their goals <>min=? (R{"time1"}[F "goal1" ] + R{"time2"}[F "goal2" ])