## Intent

Specifies that an avoidance condition globally holds.

## LTL Template

$\mathcal{G}(\neg (l_1))$, where $l_1 \in L$

## Examples and Known Uses

The robot should avoid entering location $l_1$.
Trace `$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
$l_1$.

## Relationships

Global avoidance is a specific instance of the Avoidance patterns requiring a location to be always avoided.

## Occurences

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.

## CTL Template

$\forall \mathcal{G}(\neg (l_1))$, where $l_1 \in L$