const int k; const double p; // Reachability Pmax=? [ F "goal1" ] // Bounded reachability Pmax=? [ F<=k "goal2" ] // Half an LTL formula Pmax=? [ G !"hazard" ] // A simple LTL formula Pmax=? [ G F "goal1" ] // Another LTL formula Pmax=? [ (G !"hazard")&(G F "goal1") ] // Check can reach goal2 with prob 1 Pmax=? [ F "goal2" ] // Rewards: best exp time to reach goal2 R{"time"}min=? [ F "goal2" ] // Pareto multi(Pmax=? [ G !"hazard" ], Pmax=? [ G F "goal1" ]) // Pareto (swap axes) multi(Pmax=? [ G F "goal1" ], Pmax=? [ G !"hazard" ]) // Approximate Pareto with numerical multi(Pmax=? [ G F "goal1" ], P>=p [ G !"hazard" ]) // Approximate Pareto with numerical (swap axes) multi(Pmax=? [ G !"hazard" ], P>=p [ G F "goal1" ])