Intent
The robotic application shall keep the value of the quantitative measure m greater than or equal to v while performing a mission miss.
Template
The following formulae encode the mission in PCTL and CSRL depending on whether the quantitative measure represents the probability of achieving a mission or the reward collected while performing the mission.
PCTL – Probability
$
\mapping(\term{m}\ \lit{at least}\ \terminal{\val} \ \term{miss})=\LTLp_{\geq \terminal{\val} }(\mapping(\term{miss}))
$
CSRL – Reward
$
\mapping(\term{m}\ \lit{at least}\ \terminal{\val} \ \term{miss})=\mathcal{E}_{[v,\infty)}(\mapping(\term{miss}))
$
Variations
Examples and Known Uses
A rover on a science exploration […] is exploring an area looking for an object of interest for scientific studies. […] the goal would be to plan a path such that it gets connected with a minimum expected traveled distance [57]
Relationships
See the at most and [strict] bounding patterns.