Intent
The robotic application shall keep the value of the quantitative measure m within the (open) interval [v1, v2] 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{strictly within}\ \term{\val 1}\ \lit{and}\ \term{\val 2}\ \term{miss})=\LTLp_{> \terminal{\val} _1}(\mapping(\term{miss})) \wedge \LTLp_{< \terminal{\val} _2}(\mapping(\term{miss}))
$
CSRL – Reward
$
\mapping(\term{m}\ \lit{strictly within}\ \term{\val 1}\ \lit{and}\ \term{\val 2}\ \term{miss})=
\mathcal{E}_{(\terminal{\val} _1,\infty)}
(\mapping(\term{miss}))
\wedge
\mathcal{E}_{[0,\terminal{\val} _2)}
(\mapping(\term{miss}))
$
Variations
Examples and Known Uses
Relationships
See the at least, at most and bounding patterns.