$ \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} $

QUARTET: QUANTITATIVE ROBOTIC SPECIFICATION PATTERNS

• Pattern Catalog
• QUARTET DSL
• QUARTET TOOL
• Requirements Collection
• Evaluation
• Authors