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 \rightarrow \mathcal{X} (p_2))$, where $p_1 \in M$ and $p_2 \in PL \cup PA$
Examples and Known Uses
If $c$ occurs $l_1$ is reached in the next time instant.
The trace $l_1 \rightarrow l_3 \rightarrow \{l_2,c\} \rightarrow l_1 \rightarrow l_4 \rightarrow (l_3)^\omega$ satisfies the mission requirement, since after $c$ occurs $l_1$ is reached within the next time instant.
The trace $l_1 \rightarrow$ $l_3 \rightarrow \{l_2,c\} \rightarrow l_4 \rightarrow l_1 \rightarrow (l_3)^\omega$ does not satisfy the mission requirement.
CTL Template
$\forall \mathcal{G}( p_1 \rightarrow \forall \mathcal{X} (p_2))$, where $p_1 \in M$ and $p_2 \in PL \cup PA$