Intent
The robotic application shall keep the value of the quantitative measure m strictly greater than 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{greater than}\ \terminal{\val} \ \term{miss})=\LTLp_{> \terminal{\val} }(\mapping(\term{miss}))
$
CSRL – Reward
$
\mapping(\term{m}\ \lit{greater than}\ \terminal{\val} \ \term{miss})=\mathcal{E}_{(v,\infty)}(\mapping(\term{miss}))
$
Variations
Examples and Known Uses
Relationships
See the at least, at most and [strict] bounding patterns.