QUARTET DSL: Syntax

The grammar of the QUARTET DSL is below. Optional items are enclosed in round brackets labeled with the ? character; the symbol | separates alternatives. The terminals of the language are loc, rob, condition, act, m, and v. The terminal loc represents a location: either a logical location, e.g., a room of the building, or a physical location, e.g., position x, y, z . The terminal rob indicates a robot. The terminal condition represents Boolean condition that is true or false. The terminals act, act1 , act2 , . . . , actn indicate actions. The terminal m represents a quantitative measure. The terminals v, v1 ,v2 are values. A robotic mission can be specified as a the conjunction of two missions (miss and miss), disjunction of two missions (miss or miss), negation of a mission (not miss), a non- quantitative pattern describing the task to be executed by a robot (rob shall pat), an elementary quantitative pattern (e_qpat), or a composite quantitative pattern (c_qpat).

QUARTET DSL: Semantics

We define the semantics by proposing a translation that maps the constructs of the DSL that refer to patterns from the QUARTET catalogue into PRCTL formulae. For the semantics of the constructs of the DSL that refer to the 22 non-quantitative robotic mission specification patterns the reader can refer to. roboticpatterns.

One can observe the translation τ defining our semantics. The table is divided into three parts containing respectively the semantics of the mission, elementary patterns, and composite patterns constructs. The translation τ defines how to convert each operator of our language into PRCTL. For example, the PRCTL formula obtained by applying

the mapping function τ to the formula miss and miss is the formula τ (miss) ∧ τ (miss), i.e., the conjunction of the PRCTL formulae obtained by appling the translation τ to the left and the right operands of the and operator.

For mission constructs, the definition of the translation τ specifies how to convert the Boolean operators that define the mission into the corresponding PRCTL operators. For the construct rob shall pat, the PRCTL formula generated by the translation (τ (pat[r ← − rob])) is obtained by applying the translation to the term pat and by associating the value of the term rob to the variable r, that will be later defined, during the translation.

QUARTET DSL: Usage

The usage of the elementary and composite patterns of the QUARTET catalogue is enabled by the terms epat and cpat. Each alternative in the rule of the term epat enables using one of the elementary patterns. Each alternative in the rule of the term cpat enables using one of the composite patterns. The construct associated to each mission specification problem is reported below (column DSL).

Consider the following mission requirement:

After closure, the robot r1 shall visit the different parts of the shop to record the items that are present on the shelves after closure. The robots have to minimize the time required to perform this mission

This can be expressed as follows:

minimize time (
(r1 shall react instantly to clos by visit {CP,TA,HA})
and
(r1 shall counteract instantly to (r1 in CP) by record)
and
(r1 shall counteract instantly to (r1 in TA) by record)
and
(r1 shall counteract instantly to (r1 in HA) by record) )