$ \newcommand{\LTLf}{\mathcal{F}} \newcommand{\lit}[1]{\textbf{#1}} \newcommand{\term}[1]{\texttt{#1}} \newcommand{\terminal}[1]{\textup{#1}} \newcommand{\mapping}{\tau} \newcommand{\translation}{\tau} \DeclareMathOperator{\LTLb}{\mathcal{B}} \DeclareMathOperator{\measure}{\mathcal{m}} \DeclareMathOperator{\LTLcirclew}{\LTLcircle_w} \DeclareMathOperator{\LTLcircleminusw}{\LTLcircleminus_w} \DeclareMathOperator{\LTLu}{\mathcal{U}} \DeclareMathOperator{\LTLuw}{\mathcal{U}_w} \DeclareMathOperator{\LTLb}{\mathcal{B}} \DeclareMathOperator{\LTLr}{\mathcal{R}} \DeclareMathOperator{\LTLs}{\mathcal{S}} \DeclareMathOperator{\LTLsw}{\mathcal{S}_w} \DeclareMathOperator{\LTLw}{\mathcal{W}} \DeclareMathOperator{\LTLf}{\mathcal{F}} \DeclareMathOperator{\LTLg}{\mathcal{G}} \DeclareMathOperator{\LTLx}{\mathcal{X}} \DeclareMathOperator{\LTLxw}{\mathcal{X}_w} \DeclareMathOperator{\LTLp}{\mathcal{P}} \DeclareMathOperator{\LTLpw}{\mathcal{P}_w} \DeclareMathOperator{\LTLh}{\mathcal{H}} \DeclareMathOperator{\LTLo}{\mathcal{O}} \DeclareMathOperator{\LTLpredict}{\rhd} \DeclareMathOperator{\LTLrecord}{\lhd} \DeclareMathOperator{\LTLstop}{stop} \DeclareMathOperator{\LTLimplication}{\rightarrow} \DeclareMathOperator{\LTLequivalent}{\leftrightarrow} \DeclareMathOperator{\LTLand}{\wedge} \DeclareMathOperator{\LTLor}{\vee} \DeclareMathOperator{\LTLfalse}{\bot} \DeclareMathOperator{\LTLtrue}{\top} $

Quantitative Specification Patterns for Robotic Missions

This page complements the manuscript "Robotic Mission Specification Patterns: Providing Support for Quantitative Properties" and is an online repository of a quantitative specification pattern catalog for missions of mobile robots, along with an accompanying DSL and tool support: QUARTET. The pattern system is not intended to be exhaustive or complete, and the repository is not intended to be static. The set of patterns will grow over time as designers specify missions that do not belong to the provided patterns.

You can further find the patterns, information on requirements collection as well as DSL and tool support through QUARTET. Reproduction kits, specifications and accompanying code can be found in evaluation. See also an introductory video to QUARTET.

Pattern Catalog

catalog

Elementary Patterns

Elementary mission specification problems capture fundamental quantitative measures.

Pattern Description
Maximise Maximize m while performing the mission miss.
Minimise Minimize m while performing the mission miss.
At most Keep m lower than or equal to v while performing miss.
Less than Keep m strictly lower than v while performing miss.
At least Keep m greater than or equal to v while performing miss.
Greater than Keep m strictly greater than v while performing miss.
Exactly Keep m exactly v while performing miss.
Bounding the value Keep m within the (closed) interval [v1, v2] while performing miss.
Strict bounding the value Keep m within the (open) interval (v1, v2) while performing miss.

Composite Patterns

Composite mission specification problems express higher- order robotics concerns.

Pattern Description
Conservation Minimize the value of m performing miss.
Preservation Keep the value of m within interval [bl ,bu ] while performing miss.
Pause Pause the mission miss for m time instants. Then, restart it.
Timeout-deadline Execute miss. Stop the the execution when the timeout m is reached.
Repeat Repeat the mission miss every m time units.
End Terminate mission miss exactly at time m.
Proportionality Keep the time to perform miss1 and miss2 proportional by a factor p.
Simultaneously Execute the actions act1 ,act2 ,…, actn simultaneously.
Accrue Maximize the performance m while performing miss.
Reliably Ensure that the measure m is higher/lower than the value v.
Confidently Achieve miss and ensure that confidence m is higher/lower than v.
Equidistance rob performs miss by keeping rob1 and rob2 at the same distance.
Trail rob follows object o keeping a distance v.