Intent
The robotic application shall keep the value of the quantitative measure m exactly with the value of 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{exactly}\ \term{v1}\ \term{miss})=
\LTLp_{\geq v1}
(\mapping(\term{miss}))
\wedge
\LTLp_{\leq v1}
(\mapping(\term{miss}))
$
CSRL – Reward
$
\mapping(\term{m}\ \lit{exactly}\ \term{v1}\ \term{miss})=
\mathcal{E}_{\geq v1}
(\mapping(\term{miss}))
\wedge
\mathcal{E}_{\leq v1}
(\mapping(\term{miss}))
$
Variations
Examples and Known Uses
Each demand needs to be serviced exactly T time units after its generation, by a vehicle present at the demand location [58]
Relationships
See the at least, at most and [strict] bounding patterns.