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

LTL Template

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

Examples and Known Uses

The trace $l_1 \rightarrow l_3 \rightarrow \{l_2,c\} \rightarrow \{l_1\} \rightarrow \{l_4,1_1\} \rightarrow \{l_1\} \rightarrow \{l_4,a_1\} \rightarrow (l_3)^\omega$ satisfies the mission requirement. The trace $l_1 \rightarrow l_3 \rightarrow \{l_2,c\} \rightarrow \{l_1\} \rightarrow \{l_4,1_1\} \rightarrow \{l_1,a_1\} \rightarrow \{l_4\} \rightarrow (l_3)^\omega$ does not satisfy the mission requirement.

CTL Template

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