Intent

A robot must patrol a set of locations following a strict order.

LTL Template

$\mathcal{G} (\mathcal{F} (l_1 \wedge \mathcal{F}(l_2 \wedge \ldots \mathcal{F}(l_n)))) $ $\overset{n-1}{\underset{i=1}{\bigwedge}} (\neg l_{i+1}) \mathcal{U} l_i$ $\overset{n}{\underset{i=1}{\bigwedge}} \mathcal{G} (l_{(i+1)\%n} \rightarrow \mathcal{X} ( (\neg l_{(i+1)\%n}) \mathcal{U} l_{i}))$ $\overset{n-1}{\underset{i=1}{\bigwedge}} \mathcal{G} ((l_{i}) \rightarrow \mathcal{X} (\neg l_{i} \mathcal{U} (l_{(i+1)\%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 following the strict order $l_1$, $l_2$, and $l_3$. The trace $l_1 \rightarrow l_4 \rightarrow l_1 \rightarrow l_2 \rightarrow l_4 \rightarrow l_3 \rightarrow ( l_1 \rightarrow l_2 \rightarrow l_3)^\omega$ violates the mission requirement since $l_1$ is visited twice before $l_2$. The trace $l_1\rightarrow l_4 \rightarrow l_2 \rightarrow l_4 \rightarrow l_3 \rightarrow ( l_1 \rightarrow l_2 \rightarrow l_3)^\omega$ satisfies the mission requirement.

A common usage example of the Strict Sequence Patrolling pattern is a scenario where a robot is performing surveillance in a building during night hours. Strict Sequence Patrolling and Avoidance often go together. Avoidance patterns are used to force robots to avoid obstacles as they guard an area. Triggers can also be used in combination with the Strict Sequence Patrolling pattern to specify conditions upon which Patrolling should start or stop.

Relationships

The Strict Sequence Patrolling pattern is a specialisation of the Visiting pattern, in which the robot should keep visiting a set of points or locations in a given strict order.

Occurences

Smith et. al. proposed a mission specification that forces a robots to not visit a location twice in a row before a final target location is reached. This can be considered as an example of strict ordered patrolling.

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)))) $ $\overset{n-1}{\underset{i=1}{\bigwedge}} \forall (\neg l_{i+1}) \mathcal{U} l_i$ $\overset{n}{\underset{i=1}{\bigwedge}} \forall \mathcal{G} (l_{(i+1)\%n} \rightarrow \forall \mathcal{X} ( \forall (\neg l_{(i+1)\%n}) \mathcal{U} l_{i}))$ $\overset{n-1}{\underset{i=1}{\bigwedge}} \forall \mathcal{G} ((l_{i}) \rightarrow \forall \mathcal{X} (\forall \neg l_{i} \mathcal{U} (l_{(i+1)\%n})))$