## Intent

Applies when a counteraction must be performed every time and only when a specific location is entered..

## LTL Template

$(l_1) \mathcal{U} (p)$, where $l_1 \in L$ and $p \in PE \cup PA$

## Examples and Known Uses

The robot remains in location $l_1$ until condition $c$ is satisfied. The trace $l_1 \rightarrow l_3 \rightarrow { l_2,c} \rightarrow l_1 \rightarrow l_4 \rightarrow (l_3)^\omega$ violates the mission requirement since the robot left $l_1$ before condition $c$ is satisfied. The trace $l_1 \rightarrow {l_1,c} \rightarrow l_2 \rightarrow l_1 \rightarrow l_4 \rightarrow (l_3)^\omega$ satisfies the mission requirement.

## CTL Template

$\forall (l_1) \mathcal{U} (p)$, where $l_1 \in L$ and $p \in PE \cup PA$