Intent

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

LTL Template

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