Specifies that an avoidance condition globally holds.
Examples and Known Uses
The robot should avoid entering location $l_1$.
$l_3 \rightarrow l_4 \rightarrow l_3 \rightarrow l_2 \rightarrow l_4 \rightarrow l_3 \rightarrow ( l_3 \rightarrow l_2 \rightarrow l_3)^\omega$, satisfies the mission requirement since the robot never enters
Global avoidance is a specific instance of the Avoidance patterns requiring a location to be always avoided.
LTL formulation of avoidance has been proposed in many papers, such as Wang et al.
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.