## Intent

Applies when the occurrence of a stimulus instantaneously triggers a counteraction.

## LTL Template

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

## Examples and Known Uses

When location $l_2$ is reached action $a$ must be executed. The trace $l_1 \rightarrow l_3 \rightarrow \{ l_2,a \} \rightarrow \{ l_2,a \} \rightarrow l_4 \rightarrow (l_3)^\omega$ satisfies the mission requirement since when location $l_2$ is entered condition $a$ is performed. The trace $l_1 \rightarrow l_3 \rightarrow l_2 \rightarrow \{l_1,a\} \rightarrow l_4 \rightarrow (l_3)^\omega$ does not satisfy the mission requirement since when $l_2$ is reached $a$ is not executed.

## Relationships

The LTL formula used to encode Instantaneous Reaction Pattern is an example of Reaction Pattern in which the reaction occurs instantaneously.

## Occurences

An example of usage of instantaneous reaction is used by Fainekos et al. to specify the mission requirement: if you reach room l1, perform a collaborative grasping action.

## Büchi Automaton representing accepting sequences of events

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 p_2)$, where $p_1 \in M$ and $p_2 \in PL \cup PA$