Intent

The robotic application shall keep the value of the quantitative measure m within the (closed) 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{within}\ \term{v1}\ \lit{and}\ \term{v2}\ \term{miss})= \LTLp_{\geq \terminal{\val} _1}(\mapping(\term{miss})) \wedge \LTLp_{\leq \terminal{\val} _2}(\mapping(\term{miss})) $
CSRL – Reward
$ \mapping(\term{m}\ \lit{within}\ \term{v1}\ \lit{and}\ \term{v2}\ \term{miss})= \mathcal{E}_{[\terminal{\val} _1,\infty)} (\mapping(\term{miss})) \wedge \mathcal{E}_{[0,\terminal{\val} _2]} (\mapping(\term{miss}))$} $

Variations

This pattern can be extended by providing a strict bound.

Examples and Known Uses

We assume a set of robots […] we have a set of tasks each with a location, an earliest start time, a latest finish time, and a duration for each task. […] Robots need to arrive to a task after it earliest start time and before its latest start time […] [59] robots move at 10 m/s and encounter a traffic signal at every 300 m whose waiting time is [..] [60]

Relationships

See the at least, at most and [strict] bounding patterns.