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

$\overset{n}{\underset{i=1}{\bigwedge}} \mathcal{G}( \mathcal{F} (l_i))$ $\overset{n}{\underset{i=1}{\bigwedge}} \mathcal{G} (l_{i} \rightarrow \mathcal{X} ((\neg l_i)\ \mathcal{W}\ l_{(i+1)\%n}))$ , where ($l_1, l_2, \ldots$ are location propositions)

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.

CTL Template

$\overset{n}{\underset{i=1}{\bigwedge}} \forall \mathcal{G}( \forall \mathcal{F} (l_i))$ \\ $\overset{n}{\underset{i=1}{\bigwedge}} \forall \mathcal{G} (l_{i} \rightarrow \forall \mathcal{X} (\forall (\neg l_i) \mathcal{W} l_{(i+1)\%n}))$