Intent
This pattern requires a robot to keep visiting a set of locations, in some specified order, similarly to sequenced patrolling. However, given an order, e.g., 1 and 2 between two locations, it is not admitted to the robot to visit 2 before 1.
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
Locations $l_1$, $l_2$, and $l_3$ must be patrolled following the order $l_1$, $l_2$, and $l_3$.
The trace $l_1\rightarrow l_4 \rightarrow l_3 \rightarrow l_1 \rightarrow l_4 \rightarrow l_2 \rightarrow ( l_1 \rightarrow l_2 \rightarrow l_3)^\omega$ violates the mission requirement since $l_3$ precedes $l_2$.
The trace $l_1 \rightarrow l_1 \rightarrow l_2 \rightarrow l_4 \rightarrow l_4 \rightarrow l_3 \rightarrow ( l_1 \rightarrow l_2 \rightarrow l_3)^\omega$ satisfies the mission requirement.
Relationships
The Ordered Patrolling pattern specializes Sequenced Patrolling by requiring locations to be visited in order.
Occurences
An example of ordered patrolling can be obtained by combining the sequence patrolling formulation provided by Chen 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.