Intent
Applies when the occurrence of a stimulus instantaneously triggers a counteraction.
LTL Template
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.