Intent
Keep visiting a set of locations, but not in a particular order.
LTL Template
Note that the pattern is general and consider the case in which a robot can be in two locations at the same time. For example, a robot can be in an area of a building indicated as l1 (e.g., area 01) and at the same time in a room of the area indicated as l2 (e.g., room 002) at the same time. If the topological intersection of the considered locations is empty, then the robot cannot be in two locations at the same time and the transitions labeled with both l1 and l2 cannot be fired.
Examples and Known Uses
This pattern also appears in literature as surveillance. It is used to encode infinite executions of the robot, such as surveillance, persistent monitoring, and pickup-delivery missions.
Locations $l_1$, $l_2$, $l_3$ must be surveilled.
The trace $l_1 \rightarrow l_4 \rightarrow l_3 \rightarrow l_1 \rightarrow l_4 \rightarrow l_2 \rightarrow (l_2 \rightarrow l_3 \rightarrow l_1)^\omega$ ensures that the mission requirement is satisfied.
The trace $l_1 \rightarrow l_2 \rightarrow l _3 \rightarrow (l_1 \rightarrow l_3)^\omega$ represents a violation, since $l_2$ is not surveilled.
Relationships
The Patrolling pattern generalizes the Visit pattern by requiring to keep visiting a set of areas.
Occurences
Wolff et al. provides an LTL specification to encode a mission requirement requiring that two locations must be visited repeatedly. It also propose an LTL property specifying that an agent should keep entering a location. These specifications can be considered as instances of the survillance pattern. Smith et al. proposed a mission requirement that forces robots to repeatedly visit a set of locations. This is an example of usage of the patrolling pattern.
Büchi Automaton representing accepting sequences of events
where circled states are accepting states and states with an incoming arrow with no source are initial states. The automaton above is deterministic.