Intent
This pattern requires a robot to keep visiting a set of locations in a fair way, i.e., the robots patrols the locations by keeping the number of times every area is patrolled equal.
LTL Template
where “l1” and “l2” are expressions that indicate that a robot r is in location 1 and 2. The specification given locations 1 and 2 to be visited fairly, requires that after 1 is visited, 1 is not visited again before 2. This is a necessary approximation since LTL does not allow counting, ensuring that the difference on the number of times locations 2 and 1 are visited is at most one.
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$, and $l_3$ must be fair patrolled.
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_1 \rightarrow l_3)^\omega$
violates the mission requirements since the robot patrols $l_1$ more than $l_2$ and $l_3$.
The trace $l_1 \rightarrow l_4 \rightarrow l_3 \rightarrow l_4 \rightarrow l_2 \rightarrow l_4 \rightarrow ( l_1 \rightarrow l_2 \rightarrow l_3)^\omega$
satisfies the mission requirement since locations $l_1$, $l_2$, and $l_3$ are patrolled fairly.
Relationships
The Fair Patrolling pattern is a specialization of the Patrolling pattern, in which the robot should keep visiting a set of locations in a fair way.
Occurences
Smith et al. proposed an instance of mission specification that requires an equal number of visits to each data-gathered location.
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.