Mission Specification Patterns for Mobile Robots: Providing Support for Quantitative Properties

Claudio Menghi, Christos Tsigkanos, Mehrnoosh Askarpour, Patrizio Pelliccione, Gricel Vazquez, Radu Calinescu, Sergio Garcia

Research output: Contribution to journalArticlepeer-review


With many applications across domains as diverse as logistics, healthcare, and agriculture, service robots are in increasingly high demand. Nevertheless, the designers of these robots often struggle with specifying their tasks in a way that is both human-understandable and sufficiently precise to enable automated verification and planning of robotic missions. Recent research has addressed this problem for the functional aspects of robotic missions through the use of mission specification patterns. These patterns support the definition of robotic missions involving, for instance, the patrolling of a perimeter, the avoidance of unsafe locations within an area, or reacting to specific events. Our paper introduces a catalog of QUantitAtive RoboTic mission spEcificaTion patterns (QUARTET) that tackles the complementary and equally important challenge of specifying the reliability, performance, resource use, and other key quantitative properties of robotic missions. Identified using a methodology that included the analysis of 73 research papers published in 17 leading software engineering and robotics venues between 2014–2021, our 22 QUARTET patterns are defined in a tool-supported domain-specific language. As such, QUARTET enables: (i) the precise definition of quantitative robotic-mission requirements; and (ii) the translation of these requirements into probabilistic reward computation tree logic (PRCTL), and thus their formal verification and the automated planning of robotic missions. We demonstrate the applicability of QUARTET by showing that it supports the specification of over 95% of the quantitative robotic mission requirements from a systematically selected set of recent research papers, of which 75% can be automatically translated into PRCTL for the purposes of verification through model checking and mission planning.
Original languageEnglish
Number of pages20
JournalIEEE Transactions on Software Engineering
Publication statusAccepted/In press - 5 Dec 2022

Bibliographical note

This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details

Cite this