Intent

The robotic application shall maximize 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{maximize}\ \term{m}\ \term{miss})= \mathcal{P}_{max=?}( \LTLf (\mapping(\term{miss}))) $
CSRL – Reward
$ \mapping(\lit{maximize}\ \term{m}\ \term{miss})=\mathcal{E}_{max=?}( \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

“Given a team of robots […] find a control strategy for the robotic team that yields the maximum probability of satisfying the task [36]”.

Relationships

The Maximize pattern can be used in combination with the Interval and Bound patterns to set upper and lower bounds for the maximization.

Occurences

Kloetzer and Mahulea [36] proposed a mission specification forcing a team of robots to find a strategy for the robots that yields the maximum probability of satisfying the task.