We evaluate the coverage of the QUARTET patterns (RQ1), the applicability of our translation (RQ2), and the exploitability of the logic formulae generated by our translation (RQ3).
RQ1 assesses coverage; patterns are designed to cover recurrent robotic mission specification problems. Therefore, they are not exhaustive. Given a test set of mission requirements, RQ1 verifies whether our patterns can express these requirements.
RQ2 assesses the applicability of our translation method in practice; Since our translation considered probability and rewards as quantitative measures interpretations and PRCTL as target logic, it does not support some of the DSL constructs. In addition, due to the limitations of the language of PRISM, we add a set of constraints to ensure that specification is within the PRISM input language. RQ2 assesses how these factors limit the applicability of our translation in practical cases.
RQ3 assesses the usefulness of our mission specification in practical scenarios. The mission specification generated by our translation (e.g., the PRCTL formula) supports automated reasoning (e.g., as an input for model checking and synthesis tools).