// to check properties need to use the digital clocks engine const int T; // time bound in properties // minimum expected time to reach goal2 R{"time"}min=? [ F "goal2" ] // maximum expected time to reach goal2 R{"time"}max=? [ F "goal2" ] // maximum probability of reaching a goal1 state by time T Pmax=?[ F<=T "goal1" ] // maximum probability of reaching a goal2 state by time T Pmax=?[ F<=T "goal2" ]