Intent
The robotic application shall minimise the value of the quantitative measure m 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(\lit{minimize}\ \term{m}\ \term{miss})=\mathcal{P}_{min=?}( \LTLf (\mapping(\term{miss})))
$
CSRL – Reward
$
\mapping(\lit{minimize}\ \term{m}\ \term{miss})=\mathcal{E}_{min=?}( \LTLf( \mapping(\term{miss})))
$
Variations
This pattern can be extended by considering other quantitative measures, such as energy saving and utility.
Examples and Known Uses
picks up an object at an initial position and moves it to a final position, minimizing the time [55]
Relationships
The Minimise pattern can be used in combination with the Interval and Bound patterns to set upper and lower bounds for the minimization.