DelayedImplication

Delayed Implication

Delayed Implication
INTENTION This pattern is applicable if one phenomenon, represented by the formula $\psi$, always depends in the positive case on another phenomenon, represented by the formula $\varphi$, with a maximal time delay $\tau$.
SIGNATURE $\mathcal{V}^{\mathit{fo}} = \{\varphi, \psi\}$, $\mathcal{V}^{\mathit{fu}} = \emptyset$, $\mathcal{V}^{\mathit{te}} = \emptyset$, $\mathcal{V}^{\mathit{ti}} = \{\tau\}$
FORMAL $\square( \varphi \Rightarrow_{\le \tau} \psi)$
NATURAL LANGUAGE Whenever $\varphi$ holds continuously for at least $\tau$ time units, then eventually within this time span, $\psi$ is true and remains true at least as long as $\varphi$ holds.
Examples
EXAMPLE 1
  FORMAL $\square( \mathit{hazardousCondition} \Rightarrow_{\le 30} \mathit{windowClosed})$
  NATURAL
LANGUAGE		 Whenever a hazardous condition holds continuously for at least 30 seconds, the eventually within this time span, the window is closed and remains closed at least as long as the hazardous condition continues.
Theorem Part
THEOREM SIGNATURE $\mathcal{V}^{\mathit{fo}} = \{\varphi_1, \varphi_2, \varphi_3, \psi_1, \psi_2\}$, $\mathcal{V}^{\mathit{fu}} = \emptyset$, $\mathcal{V}^{\mathit{te}} = \emptyset$, $\mathcal{V}^{\mathit{ti}} = \{\tau_1, \tau_2\}$
THEOREM 1 Transitivity
  FORMAL $(\square( \varphi_1 \Rightarrow_{\le \tau_1} \varphi_2) \wedge \square( \varp... ..._3)) \rightarrow \square( \varphi_1 \Rightarrow_{\le \tau_1+\tau_2} \varphi_3)$
  EXPLANATION This theorem expresses the transitivity of this pattern.
THEOREM 2 Conclusion Distributivity over $\wedge$
  FORMAL $(\square( \varphi_1 \Rightarrow_{\le \tau_1} \psi_1) \wedge \square( \varphi_1... ...rightarrow \square( \varphi_1 \Rightarrow_{\le \tau_1} (\psi_1 \wedge \psi_2))$
  EXPLANATION This theorem expresses the distributivity over $\wedge$ of the conclusions of two instantiations of this pattern.




 Superordinated page: Pp

 Feedback
Go to the contact details of the person in charge of this page

 Deutsch
This page in german. Diese Seite auf deutsch.