Intent

Given a set of locations the robot should visit all the locations following a strict order.

LTL Template

$\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-1}{\underset{i=1}{\bigwedge}} (\neg l_{i}) U (l_i \wedge \mathcal{X} (\neg l_{i} \mathcal{U} (l_{i+1})))$, where $l_1, l_2, \ldots$ are location propositions.

Ordered visit pattern does not avoid a predecessor location to be visited multiple times before its successor. Strict ordered visit forbids this behavior.

Examples and Known Uses

This problem is also indicated in literature as strict ordered reach, cover, or search, meaning that a robot should reach, cover or search a set areas or points following a strict order.

Locations $l_1$, $l_2$, $l_3$ must be covered following the strict order $l_1$, $l_2$, $l_3$. The trace $l_1 \rightarrow l_4 \rightarrow l_1 \rightarrow l_2 \rightarrow l_4 \rightarrow l_3 \rightarrow (l_{\#})^\omega$ does not satisfy the mission requirement since $l_1$ occurs twice before $l_2$. The trace $l_1 \rightarrow l_4 \rightarrow l_2 \rightarrow l_4 \rightarrow l_3 \rightarrow (l_{\#})^\omega$ satisfies the mission requirement.

Strict Ordered visit can be used in combination with Avoidance and Trigger patterns. Avoidance patterns are used to force robots to e.g. avoid obstacles as they guard an area. Trigger can also be used in combination with the Visit pattern to specify conditions upon which Visit should start or stop.

Relationships

The Strict Ordered visit pattern specializes the Ordered visit pattern by further constraining how locations are visited.

Occurences

Smith et al. proposed a mission requirement that forces a robots to not visit a location twice in a row before a final target location is reached, i.e., it forgives l1 to be visited twice before l2. This constraint combined with the sequenced visit pattern allows the realization of a strict sequenced visit.

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