Specifies that a condition will be avoided in the future.

LTL Template

$\mathcal{G}( (c) \rightarrow( \mathcal{G} (\neg (l_1))))$, where $c \in M$ and $l_1 \in PL$

Examples and Known Uses

If the robot enters $l_1$, then it should avoid entering $l_2$ in the future. The trace $l_3 \rightarrow l_4 \rightarrow l_3 \rightarrow l_1 \rightarrow l_4 \rightarrow l_3 \rightarrow ( l_3 \rightarrow l_2 \rightarrow l_3)^\omega$ does not satisfy the mission requirement since $l_2$ is entered after $l_1$.


The LTL formula used to encode Future avoidance corresponds to the formula used to encode the Response pattern of Dwyer et al., scoped with the glocal operator


An example of use of the future avoidance pattern has been used by Wong et specify that if “Alice is on the bridge then next bob cannot be on the square” and by Smith et al. to specify that a task cannot be followed by another. An example of usage of the future avoidance pattern has been discussed also by Chen et al. that states that during each cycle a task cannot follow another.

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}( (c) \rightarrow( \forall \mathcal{G} (\neg (l_1))))$, where $c \in M$ and $l_1 \in PL$