Given a set of locations the robot should REPEATEDLY visit all the locations in sequence.

LTL Template

$\mathcal{G} (\mathcal{F} (l_1 \wedge \mathcal{F}(l_2 \wedge \ldots \mathcal{F}(l_n))))$ , where ($l_1, l_2, \ldots$ are location propositions)

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$, $l_3$ must be patrolled in sequence. %, 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$ satisfies the mission requirement since globally any $l_1$ will be followed by $l_2$ and $l_2$ by $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_3)^\omega$ violates the mission requirement since after visiting $l_1$, the robot does not visit $l_2$.


The Sequenced Patrolling pattern specializes the Patrolling by requiring locations to be visited in sequence.


An example of mission specification that solves the sequence patrolling problem has been provided by Chen et al. that proposed a formula specifying that two tasks are performed in sequences, and one of them must occur at least once before the other.

Büchi Automaton representing accepting sequences of events

alt text

where circled states are accepting states and states with an incoming arrow with no source are initial states. The automaton above is deterministic.

CTL Template

$\forall \mathcal{G} (\forall \mathcal{F} (l_1 \wedge \forall \mathcal{F}(l_2 \wedge \ldots \forall \mathcal{F}(l_n))))$