Intent

Given a set of locations the robot should visit all the locations.

LTL Template

$\overset{n}{\underset{i=1}{\bigwedge}} F (l_i)$, where $l_1, l_2, \ldots$ are location propositions.

Examples and Known Uses

Locations $l_1$, $l_2$, and $l_3$ must be visited. $ l_1 \rightarrow l_4 \rightarrow l_3 \rightarrow l_1 \rightarrow l_4 \rightarrow l_2 \rightarrow (l_{\#})^\omega $ is an example trace that satisfies the mission requirement.

A common usage example of the Visit pattern is a scenario in which a robot has to collect a set of items that are placed in different locations and bring them in a target destination. Visit and Avoidance patterns often go together. Avoidance patterns are used e.g. to require robots to avoid obstacles as they guard an area. Trigger patterns can also be used in combination with the Visit pattern to specify conditions upon which Visit should start or stop.

Relationships

The Visit pattern generalizes most of the core movement patterns that constrain how locations are visited.

Occurences

Yoo et al. and Kress-Gazit et al. formulate an LTL mission specification to ensure that a set of areas are visited. In the first case, the visiting pattern is combined with the specification of past and future avoidance mission requirements. In the second case, an LTL mission specification is provided to describe the following mission requirement: the robot must go to rooms $P1$, $P2$, $P3$ and $P4$ in any order.

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

$\overset{n}{\underset{i=1}{\bigwedge}} \forall F (l_i)$