LazyReaction

Lazy Reaction

Lazy Reaction
INTENTION		This pattern is applicable if the truth value of phenomenon, represented by $\varphi$ (usually instantiated by a predicate symbol), is defined in dependence on another phenomenon, represented by $\psi$ . The kind of dependence considered here means, that the phenomenon represented by $\psi$ has to be true for a specific time span in the past.
SIGNATURE		$\mathcal{V}^{\mathit{fo}} = \{\varphi, \psi\}$ , $\mathcal{V}^{\mathit{fu}} = \emptyset$ , $\mathcal{V}^{\mathit{te}} = \emptyset$ , $\mathcal{V}^{\mathit{ti}} = \{\tau_1, \tau_2, \tau_3\}$
FORMAL		$\square( \varphi \leftrightarrow (\blacksquare_{\le \tau_1} \psi) \vee (\langl... ..._2} \psi ] \Rightarrow \rangle \blacksquare\blacklozenge_{\le \tau_3} \psi) )$
NATURAL LANGUAGE		$\varphi$ always holds if and only if one of the following conditions holds: during the past $\tau_1$ time units $\psi$ has continuously been true there has already been a time span of length $\tau_1 + \tau_2$ time units such that $\psi$ has continuously been true, and since this has been the case for the last time, periods where $\psi$ was false continously were not longer than or equal to $\tau_3$ .
Examples
EXAMPLE 1
	FORMAL	$\square( \mathit{roomUsed} \leftrightarrow ((\blacksquare_{\le \tau_1} \neg \mathit{roomEmpty}) \vee$ $(\langle * [ \blacksquare_{\tau_1 + \tau_2} \neg \mathit{roomEmpty} ] \Rightarrow \rangle \blacksquare\blacklozenge_{\le \tau_3} \neg \mathit{roomEmpty}) ))$
	NATURAL LANGUAGE	A room is currently in use (represented by $\mathit{roomUsed}$ if and only if one of the following conditions holds: during the past $\tau_1$ time units a room has continously been not empty; there has already been a time span of length $\tau_1 + \tau_2$ time units such that a room has continuously been not empty, and since this has been the case for the last time, periods where the room was empty continously were not longer than or equal to $\tau_3$ .
Theorem Part
THEOREM SIGNATURE		$\mathcal{V}^{\mathit{fo}} = \{\varphi, \psi\}$ , $\mathcal{V}^{\mathit{fu}} = \emptyset$ , $\mathcal{V}^{\mathit{te}} = \emptyset$ , $\mathcal{V}^{\mathit{ti}} = \{\tau_1, \tau_2, \tau_3\}$
THEOREM 1 Simplification 1
	FORMAL	$\square(\tau_1 = 0 \wedge \tau_2 = 0 \wedge \tau_3 = 0) \rightarrow$ $(\square( \varphi \leftrightarrow (\blacksquare_{\le \tau_1} \psi) \vee (\lang... ...} \psi ] \Rightarrow \rangle \blacksquare\blacklozenge_{\le \tau_3} \psi) ) )$ $\leftrightarrow(\square( \varphi \leftrightarrow \psi ))$
	EXPLANATION	This theorem expresses in which way this pattern can be simplified if all time designators are 0.
THEOREM 2 Simplification 2
	FORMAL	$\square(\tau_2 = 0 \wedge \tau_3 = 0) \rightarrow$ $(\square( \varphi \leftrightarrow (\blacksquare_{\le \tau_1} \psi) \vee (\lang... ...} \psi ] \Rightarrow \rangle \blacksquare\blacklozenge_{\le \tau_3} \psi) ) )$ $\leftrightarrow(\square( \varphi \leftrightarrow \blacksquare_{\le \tau_1} \psi ))$
	EXPLANATION	This theorem expresses in which way this pattern can be simplified if the time designators $\tau_2$ and $\tau_3$ are 0.
THEOREM 3 Simplification 3
	FORMAL	$\square(\tau_2 = 0) \rightarrow$ $(\square( \varphi \leftrightarrow (\blacksquare_{\le \tau_1} \psi) \vee (\lang... ...} \psi ] \Rightarrow \rangle \blacksquare\blacklozenge_{\le \tau_3} \psi) ) )$ $\leftrightarrow(\square( \varphi \leftrightarrow (\langle * [ \blacksquare_{\l... ...1} \psi ] \Rightarrow \rangle \blacksquare\blacklozenge_{\le \tau_3} \psi) ))$
	EXPLANATION	This theorem expresses in which way this pattern can be simplified if the time designator $\tau_2$ is 0.
THEOREM 4 Simplification 4
	FORMAL	$\square(\tau_1 = 0 \wedge \tau_2 = 0) \rightarrow$ $(\square( \varphi \leftrightarrow (\blacksquare_{\le \tau_1} \psi) \vee (\lang... ...} \psi ] \Rightarrow \rangle \blacksquare\blacklozenge_{\le \tau_3} \psi) ) )$ $\leftrightarrow(\square( \varphi \leftrightarrow \blacklozenge_{\le \tau_3} \psi ))$
	EXPLANATION	This theorem expresses in which way this pattern can be simplified if the time designators $\tau_1$ and $\tau_2$ are 0.