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

alt text

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$