Intent
Given a set of locations the robot should visit all the locations in sequence.
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 problem is also indicated in literature as reach, cover, or search, meaning that a robot should reach, cover or search a set areas or points, one following the other. This sequence may reflect e.g., a traversal strategy. Note that given two areas a and b that must be visited in sequence by a robot r , the sequence pattern does not forbid robot r to visit b before visiting a, but only requires the robot to visit b after and a while a must be visited.
Locations $l_1$, $l_2$, $l_3$ must be covered following this sequence.
The trace $l_1 \rightarrow l_4 \rightarrow l_3 \rightarrow l_1 \rightarrow l_4 \rightarrow l_2 \rightarrow (l_{\# \setminus 3})^\omega$ violates the mission since $l_3$ does not follow $l_2$.
The trace $l_1 \rightarrow l_3 \rightarrow l_1 \rightarrow l_2 \rightarrow l_4 \rightarrow l_3 \rightarrow (l_{\#})^\omega$ satisfies the mission requirement.
Sequenced Visit and Avoidance often go together. Avoidance patterns are used to require robots to avoid obstacles as e.g. they guard an area. Triggers can also be used in combination with the Sequenced Visit pattern to specify conditions upon which Visit should start or stop.
Relationships
The Sequenced Visit pattern generalizes the Ordered visit patterns that further constrain how locations are visited.
Occurences
Yoo et al. Kress-Gazit et al. and formulate an LTL mission specification that ensures that a set of areas are visited in sequence. Specifically, an LTL mission specification is provided for the following mission requirement: visit a set of area $l1, l2 \ldots ln$ by ensuring that $l1$ is visited after (but not necessarily only after) area $l2$.
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.