Intent
The robotic application shall keep the value of the quantitative measure m lower 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 most}\ \terminal{\val} \ \term{miss})=\LTLp_{\leq \terminal{\val} }(\mapping(\term{miss}))
$
CSRL – Reward
$
\mapping(\term{m}\ \lit{at most}\ \terminal{\val} \ \term{miss})=\mathcal{E}_{[0,v]}(\mapping(\term{miss}))
$
Variations
Examples and Known Uses
[…] the planner should find a path […] that does not violate a maximum level of allowed risk [56]
Relationships
See the at least and [strict] bounding patterns.