Intent

Applies when the occurrence of a stimulus triggers a counteraction some time later.

LTL Template

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

Examples and Known Uses

When $c$ occurs the robot must start moving toward location $l_1$, and $l_1$ is subsequently finally reached. 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 the robot starts moving toward location $l_1$, and location $l_1$ is finally reached. The trace $l_1 \rightarrow l_1 \rightarrow \{ l_2, c\} \rightarrow l_3 \rightarrow (l_3)^\omega$ does not satisfy the mission requirement since $c$ occurs when the robot is in $l_2$, and $l_1$ is not finally reached.

Relationships

The LTL formula used to encode Delayed Reaction Pattern corresponds to the LTL formula used to encode the Response Pattern by Dwyer, scoped with the global operator.

Occurences

Chen et al. proposed an LTL formula that forces a service to occur at maximum a specified number of times, this can be considered as an example of usage of the upper restricted avoidance pattern.

Büchi Automaton representing accepting sequences of events

alt text

where circled states are accepting states and states with an incoming arrow with no source are initial states. The automaton above is deterministic.

CTL Template

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