Intent
Given a set of locations the robot should visit all the locations in a fair way.
LTL Template
where “l1” and “l2” are expressions that indicate that a robot r is in a specific area or at a given point.
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 covered in a fair way.
The trace $l_1 \rightarrow l_4 \rightarrow l_1 \rightarrow l_3 \rightarrow l_1 \rightarrow l_4 \rightarrow l_2 \rightarrow (l_{\# -\{1,2,3\}})^\omega$ does not perform a fair visit since it visits $l_1$ three times while $l_2$ and $l_3$ are visited once.
The trace $l_1 \rightarrow l_4 \rightarrow l_3 \rightarrow l_1 \rightarrow l_4 \rightarrow l_2 \rightarrow l_2 \rightarrow l_4 \rightarrow (l_{\# \setminus\{1,2,3\}})^\omega$ performs a fair visit since it visits locations $l_1$, $l_2$, and $l_3$ twice.
Relationships
The Fair visit pattern specializes the Visit pattern by further constraining how locations are visited to ensure a fair visit.
Occurences
Smith et al.proposed an LTL mission specification for the following mission requirement “an equal number of visits to each data-gather location” is required. The LTL mission specification is obtained by forcing an order on how the data-gathered locations are visited. However, fair visiting may be required even without the specification of an order in which the locations must be visited.
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.