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

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