## Intent

Applies when the occurrence of a stimulus triggers a counteraction promptly, i.e. in the next time instant.

## LTL Template

$\mathcal{G}( p_1 \leftrightarrow p_2)$, where $p_1 \in M$ and $p_2 \in PL \cup PA$

## Examples and Known Uses

Action $a_1$ is bound though a delay to location $l_1$. The trace $l_1 \rightarrow l_3 \rightarrow \{l_2,c\} \rightarrow \{l_1,a_1\} \rightarrow l_4 \rightarrow \{l_1,a_1\} \rightarrow (l_3)^\omega$ satisfies the mission requirement. The trace $l_1 \rightarrow l_3 \rightarrow \{l_2,c\} \rightarrow \{l_1,a_1\} \rightarrow \{l_4,a_1\} \rightarrow \{l_1,a_1\} \rightarrow (l_3)^\omega$ does not satisfy the mission requirement since $a_1$ is executed in location $l_4$.

## CTL Template

$\forall \mathcal{G}( p_1 \leftrightarrow p_2)$, where $p_1 \in M$ and $p_2 \in PL \cup PA$