const int k; // Maximum probability to reach goal 1 Pmax=? [ F "goal1" ]; // Maximum probability to reach goal 1 within k steps Pmax=? [ F<=k "goal1" ]; // Maximum probability to reach locations 4 or 5 within k steps Pmax=? [ F<=k (s=4 | s=5) ]; // Maximum probability to visit goal 1 and then goal 2 Pmax=? [ F ("goal1" & (F "goal2")) ]; // Maximum probability to visit goal 1 infinitely often and avoid the hazard Pmax=? [ (G F "goal1") & (G!"hazard") ]; // Minimum expected number of steps to reach either goal (stochastic shortest path) R{"moves"}min=? [ F ("goal1"|"goal2") ];