Intent
Given a set of locations the robot should visit all the locations in order.
LTL Template
Sequence visit does not forbid to visit a successor location before its predecessor, but only that after the predecessor is visited the successor is also visited. Ordered visit forbids a successor to be visited before its predecessor.
Examples and Known Uses
This problem is also indicated in literature as ordered reach, cover, or search, meaning that a robot should reach, cover or search a set areas or points following an order.
Locations $l_1$, $l_2$, $l_3$ must covered following this order.
The trace $l_1 \rightarrow l_3 \rightarrow l_1 \rightarrow l_2 \rightarrow l_3 \rightarrow (l_{\#})^\omega$ does not satisfy the mission requirement since $l_3$ preceeds $l_2$.
The trace $l_1 \rightarrow l_4 \rightarrow l_1 \rightarrow l_2 \rightarrow l_4 \rightarrow l_3 \rightarrow (l_{\#})^\omega$ satisfies the mission requirement.
Ordered visit can be used in combination with Avoidance and Trigger patterns. Avoidance patterns are used to force robots to avoid obstacles as e.g. they guard an area. Triggers can also be used in combination with the Visit pattern to specify conditions upon which Visit should start or stop.
Relationships
The Ordered visit pattern generalizes the Strict Ordered Visit pattern that further constrains how locations are visited.
Occurences
An example of ordered visit can be obtained by combining the visit formulation provided by Yoo et al. and Kress-Gazit et al. , with the absence pattern proposed by Dwyer et al.
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.