PaperlayerView exact revision on arXiv

Source-linked AI summary

Specification Patterns for Robotic Missions

Claudio Menghi, Christos Tsigkanos, Patrizio Pelliccione, Carlo Ghezzi, Thorsten Berger

arXiv:1901.02077v1cs.SEcs.RO

TL;DR

Robotic missions need specifications that are both accessible to developers and precise enough for automated processing, yet domain-specific languages can be robot-bound and temporal logic difficult for non-experts. The paper presents a catalog of mission specification patterns and supporting tooling, derived from robotics requirements. Evaluations report reduced ambiguity, broad specification coverage, and successful execution of generated plans by real robots.

  • Problem

    Mission requirements need to be user-friendly yet precise, while domain-specific languages are often robot-bound and temporal-logic formulas are difficult and error-prone for non-experts to define.

    Source: §I · pp. 1–2

  • Method

    The authors derive a catalog of mission specification patterns from robotics requirements and provide tooling to compose patterns and generate LTL and CTL specifications.

    Source: §I · p. 2, B. Specification Pattern Tool Support · p. 7

  • Results

    Across 441 requirements, most were ambiguous and expressible with the patterns and pattern use reduced ambiguity; 1,154 of 1,251 mission specifications were obtainable, and plans for five industry scenarios ran correctly on real robots.

    Source: §I · p. 2

  • Takeaways & Limitations

    The patterns support creating mission requirements and specifications in realistic industry-sourced scenarios, including missions executed by robots using existing planners.

    Source: §I · p. 2, §V · p. 7

    The study is not exhaustive, and the pattern set may need to grow as robotic formal specifications and mission types change over time.

    Source: §VI · p. 10

Abstract

from arXiv · show

Mobile and general-purpose robots increasingly support our everyday life, requiring dependable robotics control software. Creating such software mainly amounts to implementing their complex behaviors known as missions. Recognizing the need, a large number of domain-specific specification languages has been proposed. These, in addition to traditional logical languages, allow the use of formally specified missions for synthesis, verification, simulation, or guiding the implementation. For instance, the logical language LTL is commonly used by experts to specify missions, as an input for planners, which synthesize the behavior a robot should have. Unfortunately, domain-specific languages are usually tied to specific robot models, while logical languages such as LTL are difficult to use by non-experts. We present a catalog of 22 mission specification patterns for mobile robots, together with tooling for instantiating, composing, and compiling the patterns to create mission specifications. The patterns provide solutions for recurrent specification problems, each of which detailing the usage intent, known uses, relationships to other patterns, and---most importantly---a template mission specification in temporal logic. Our tooling produces specifications expressed in the LTL and CTL temporal logics to be used by planners, simulators, or model checkers. The patterns originate from 245 realistic textual mission requirements extracted from the robotics literature, and they are evaluated upon a total of 441 real-world mission requirements and 1251 mission specifications. Five of these reflect scenarios we defined with two well-known industrial partners developing human-size robots. We validated our patterns' correctness with simulators and two real robots.

I. INTRODUCTION

Robotic mission engineering must reconcile user-friendly requirements with precise, unambiguous specifications, while domain-specific languages can be robot-bound and temporal logic difficult for non-experts. The paper proposes a pattern catalog and tooling to support mission specification, then evaluates the patterns on real-world requirements and specifications and tests them in simulation and on robots.

I. INTRODUCTION

  • Mission notation must be both user-friendly and precise, but domain-specific languages are often robot-bound while temporal-logic formulas are difficult and error-prone to define.Natural-language requirements can also be ambiguous; for example, visiting the kitchen and office does not necessarily specify their order.Source: §I · p. 1
  • The catalog and PsAlM support mission design with reusable patterns and tooling that automatically generates LTL and CTL specifications from requirements.Patterns include usage intent, known uses, relationships to other patterns, and temporal-logic templates; PsAlM also supports composing patterns into complex missions.Source: §I · p. 2
  • The catalog was derived from 245 textual mission requirements collected from robotics literature and provides a formal vocabulary for recurrent specification problems.The authors propose it to help developers avoid repeatedly creating ad hoc specifications.Source: §I · p. 2
  • Across 441 requirements, most were ambiguous and expressible with the patterns, and using patterns reduced ambiguity; 1,154 of 1,251 collected specifications could be obtained using them.The 441 requirements include five scenarios defined with BOSCH and PAL Robotics; generated specifications for those scenarios produced plans correctly executed by real robots.Source: §I · p. 2
  • The authors manually inspected template specifications, tested ten requirements on 12 randomly generated building models in Simbad, and checked that corresponding LTL and CTL specifications yielded the same results.Each tested requirement combined three patterns.Source: §I · p. 2

II. BACKGROUND

The background establishes the paper’s mission terminology and introduces the temporal logics used to express pattern templates. It distinguishes linear traces from branching paths and explains the role of temporal operators.

II. BACKGROUND

  • A mission requirement describes a robot’s task, while a mission specification expresses it in a logical language with precise semantics; a pattern maps a recurrent specification problem to a template solution and usage information.A catalog organizes patterns hierarchically to support browsing and selection.Source: §II · pp. 2–3
  • LTL formulas are interpreted over infinite sequences of truth assignments; X refers to the next position, and φ1 U φ2 means φ1 holds until φ2 does.The paper considers LTL and CTL because both are commonly used for robotic mission specifications.Source: §II · p. 3
  • CTL describes properties over branching sequences, using state formulas for positions and path formulas for paths; ∀ and ∃ quantify over all or some paths from the current position.CTL’s X and U operators are defined as in LTL.Source: §II · p. 3

III. METHODOLOGY

The authors derived a catalog from robotic mission requirements in the literature, grouping recurring specification problems and formulating corresponding patterns. Their process combines requirement collection and analysis with pattern formulation and organization.

Collection of Mission Requirements

  • 245 mission requirements were collected from 306 papers selected using movement-related inclusion criteria across robotics venues.The analysis considered papers from four major robotics venues over five years; each qualifying mission requirement was treated separately.Source: §III · p. 3

Identification of Mission Specification Problems

  • Two authors labeled requirements with keywords describing their specification problems, including patrol and instantaneous reaction.A patrol-and-inspection requirement was labeled for both its movement task and the required response at checkpoints.Source: §III · p. 3
  • The authors linked related keywords, removed nodes referring only to actions, and merged connected nodes describing the same problem.For example, “visit” and “reach” were treated as similar problems; action-only keywords such as “balance” were removed.Source: §III · p. 3

Catalog organization

  • The resulting mission-specification problems were organized in a tree structure to support catalog browsing.The catalog tree is shown with filled pattern nodes and non-filled category nodes.Source: §III · p. 3, Figure 1 · p. 4

Pattern Formulation

  • Each pattern specifies its intent, LTL and CTL templates, variations, known uses, relationships, and literature occurrences.For LTL patterns, the authors also designed Büchi automata to describe allowed behaviors unambiguously.Source: §III · p. 4

IV. MISSION SPECIFICATION PATTERNS

The section introduces a catalog of mission-specification patterns and PsAlM, a tool for systematic mission design. PsAlM supports describing requirements through the patterns and automatically generating mission specifications.

Catalog

  • The section presents a catalog of mission-specification patterns for engineering robotic missions.It also briefly describes one pattern.Source: §IV · p. 4

PsAlM

  • PsAlM supports developers in describing mission requirements through the proposed patterns.Source: §IV · p. 4
  • PsAlM supports the automatic generation of mission specifications.Source: §IV · p. 4

A. Mission Specification Pattern Catalog

The catalog contains 22 patterns in a tree, grouped into core movement, trigger, and avoidance patterns. The section outlines their scope and notation while noting that space limits leave some material to the appendix.

Catalog organization

Scope

Preliminaries

  • The paper defines propositions for robot locations, environmental conditions, and robot actions, then uses them to describe traces of system behavior.It also introduces shorthand for arbitrary locations and infinitely repeated sequences.Source: A. Mission Specification Pattern Catalog · p. 4

Core movement patterns

Avoidance patterns

Inst. Reaction

The reaction patterns distinguish immediate, delayed, and next-instant responses to stimuli. Their examples show how the timing of the counteraction affects whether a trace satisfies the mission requirement.

Inst. Reaction

  • An instantaneous reaction requires the counteraction when the stimulus occurs.The example satisfies the requirement when action a is performed upon reaching location l2, but not when it is omitted then.Source: Inst. Reaction · p. 6

Delayed Reaction

  • A delayed reaction requires a counteraction some time after the stimulus, with the example requiring eventual arrival at l1.A trace that does not eventually reach l1 after the stimulus fails the example requirement.Source: Delayed Reaction · p. 6

Prompt Reaction

  • A prompt reaction requires the counteraction in the next time instant after the stimulus.The example satisfies the requirement when l1 is reached next, but not when another location intervenes.Source: Prompt Reaction · p. 6

Bound Reaction

Bound Reaction requires a counteraction whenever, and only whenever, a specified location is entered. The example distinguishes an action performed at the bound location from one performed elsewhere.

Bound Reaction

  • A counteraction must be performed every time and only when a specific location is entered.In the example, action a1 is bound to location l1; a trace with a1 at l4 does not satisfy the requirement.Source: Bound Reaction · p. 6

Bound Delay

Bound Delay patterns specify when actions or inaction are required in relation to locations and stimuli. The examples distinguish compliant traces from traces that violate those timing or location conditions.

Bound Delay

  • A counteraction must occur in the next time instant whenever and only whenever a specific location is entered.The example trace satisfies the requirement when action a1 is bound to location l1, but not when it occurs at l4.Source: Bound Delay · p. 6
  • The robot must remain at l1 until condition c is satisfied; leaving l1 before c holds violates the requirement.A trace that reaches c while at l1 satisfies the requirement.Source: Bound Delay · p. 6
  • Trigger patterns express reactive robot behavior or inaction until a stimulus occurs.The Wait pattern describes inaction until the stimulus occurs.Source: Bound Delay · p. 6
  • The Strict Ordered Patrolling pattern is presented as an example of a mission specification pattern.Its definition is shown in Figure 2; further pattern details are available in the online appendix.Source: Bound Delay · p. 6

B. Specification Pattern Tool Support

PsAlM supports mission design by letting developers compose patterns and automatically convert the resulting requirements into LTL or CTL specifications. Its outputs can be used by planners, modeling tools, and model checkers.

B. Specification Pattern Tool Support

  • PsAlM transforms composed mission requirements into LTL or CTL specifications.The tool supports composing patterns with simple operators, and Figure 3 depicts its main components.Source: B. Specification Pattern Tool Support · p. 6, Figure 3 · p. 7
  • The GUI uses structured English to define requirements, with patterns as building blocks and AND and OR operators for composition.SE2PT extracts the composed patterns; PT2LTL and PT2CTL generate the corresponding specifications.Source: B. Specification Pattern Tool Support · p. 6
  • LTL specifications can feed planners, Spectra via deterministic Büchi automata, or NuSMV for model checking.Plans can then be used in Simbad simulations or performed by real robots; CTL specifications are also converted for NuSMV model checking.Source: B. Specification Pattern Tool Support · p. 7

V. EVALUATION

The evaluation tested whether the catalog could capture real-world requirements and generate specifications, and whether those specifications were correct. It found broad coverage across requirements and specifications, and confirmed correctness through partner scenarios, simulation, and model checking.

V. EVALUATION

  • Across five scenarios defined with BOSCH and PAL Robotics, PsAlM automatically generated LTL specifications without human intervention, and robots executed them using existing planners.The scenarios were developed with the industrial partners.Source: §V · p. 7
  • 370 of 436 mission requirements were expressible using the catalog; 102 were ambiguous, and alternative pattern combinations were proposed for them.For another 156 requirements judged unambiguous, the authors also proposed different pattern combinations.Source: §V · p. 8
  • Of 1216 Spectra specifications, 424 matched catalog patterns directly; other unmatched cases included initial-state properties, trigger variations, past operators, and complex formulas.The analysis found 127 initial-state properties, 442 trigger-pattern variations, 155 properties with past operators, and 69 complex formulas that could be rewritten using patterns but did not match them.Source: §V · pp. 8–9
  • The catalog’s final coverage was 92% for analyzed Spectra specifications, and it generated 1154 of 1251 specifications across the analyzed LTL and CTL sets.The 92% figure followed analysis of 1216 Spectra specifications, including properties using past temporal operators.Source: §V · p. 9
  • The authors manually inspected pattern instances and Büchi automata, then used random testing on 12 generated building scenarios.The scenarios each contained 16 locations, including 12 traversable and 4 non-traversable locations.Source: §V · p. 9
  • For LTL checks, NuSMV’s plans matched expected presence or absence, and Simbad simulation confirmed the generated plans’ correctness.Relaxing selected patterns produced cases where requirements became satisfied, further confirming specification correctness.Source: §V · p. 10
  • NuSMV returned the same verification results for LTL and CTL specifications, confirming the correctness of the CTL specifications.The authors also used NuSMV and Simbad to check plans and mission specifications in the evaluated scenarios.Source: §V · p. 10

VI. DISCUSSION AND RELATED WORK

The discussion presents the catalog as a reusable extension of property specification patterns, while noting that its coverage is not exhaustive and may need to grow. It also describes compatibility with GR(1) and complementarity with existing robotic DSLs and graphical tools.

VI. DISCUSSION AND RELATED WORK

  • The study is not exhaustive: robotic formal specifications and mission types evolve, and the catalog is expected to grow as uncovered specifications appear.The authors note that the number of requirements analyzed is in line with other approaches and consider the system’s scope quite wide.Source: §VI · p. 10
  • The patterns can express event ordering beyond robot actions and are presented as an extension of property specification patterns,.The paper describes composing precedence and response patterns to express chains involving multiple causes or effects.Source: §VI · p. 10
  • All proposed patterns are expressible in GR(1), but manually encoding them for Spectra is complex and error prone; an automatic mapping procedure could be integrated into PsAlM.Spectra supports initial, safety, and liveness guarantees in its GR(1) LTL fragment.Source: §VI · p. 10
  • The authors report no prior work on robotic mission patterns to their knowledge, distinguishing the catalog from earlier specification-pattern work, –, –.Related pattern applications cited include service-based applications, safety, and security,,.Source: §VI · pp. 10–11
  • The catalog is intended as reusable building blocks for robotic DSLs and complements graphical tools for specifying LTL formulas –.The authors note that graphical logic mission specifications could also be integrated within PsAlM.Source: §VI · p. 11

VII. CONCLUSION

The paper presents a pattern catalog for mobile-robot mission specification, identifies patterns from systematically collected literature requirements, and introduces PsAlM to support developers in designing complex missions. It evaluates the catalog’s support for defining real-world missions and the correctness of its specifications, while reserving time, space, probability, and user studies for future work.

VII. CONCLUSION

  • The catalog’s evaluation covers its support for defining real-world missions and the correctness of its mission specifications.Source: §VII · p. 11
  • The authors identify catalog patterns by analyzing mission requirements systematically collected from scientific publications.Source: §VII · p. 11
  • Future work will extend the catalog to time, space, and probability, investigate spatial logics for more complex spatial behaviors, and conduct user studies.Source: §VII · p. 11
Loading 1901.02077v1…