Specification Patterns for Robotic Missions

This page complements the paper "Specification Patterns for Robotic Missions" and is an online repository of a specification pattern catalog for missions of mobile robots. The pattern system is not intended to be exhaustive or complete, and the repository is not intended to be static. The set of patterns will grow over time as designers specify missions that do not belong to the provided patterns.

You can further find the patterns, information on evaluation, requirements collection and tool support through PsALM. Reproduction kits, specifications and accompanying code can be found in experiments.

Pattern Catalog

Patterns in Action

PsALM allows creating complex mission specifications by composing patterns:
A robot executing a mission based on Ordered Patrolling and Inst. Reaction:
LTL specification generation, model checking (NuSMV) and simulation (Simbad):


Core Movement Patterns

How robots should move within an environment can be divided in two major categories representing locations’ coverage and locations’ surveillance.

Avoidance patterns

Robot movements may be constrained in order to avoid occurrence of some behavior. Avoidance may reflect a condition or be a bound to the occurrence of some event.


Robot’s reactive behaviour based on stimuli or robot’s inaction until a stimulus occurs are expressed as trigger patterns.


More information on the evaluation page.