Intent
Specifies that a condition will be avoided in the future.
LTL Template
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$.
Relationships
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
Occurences
An example of use of the future avoidance pattern has been used by Wong et al.to 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
where circled states are accepting states and states with an incoming arrow with no source are initial states. The automaton above is deterministic.