Intent
The robotic application shall keep the value of the quantitative measure m strictly lower 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{less than}\ \terminal{\val} \ \term{miss})=\LTLp_{< \terminal{\val} }(\mapping(\term{miss}))
$
CSRL – Reward
$
\mapping(\term{m}\ \lit{less than}\ \terminal{\val} \ \term{miss})=\mathcal{E}_{[0,v)}(\mapping(\term{miss}))
$
Variations
Examples and Known Uses
move from a to b while avoiding static and dynamic obstacles in less than T time units
Relationships
See the at least, at most and [strict] bounding patterns.