DelayedEquivalence

Delayed Equivalence

Delayed Equivalence
INTENTION This pattern is applicable if one phenomenon, represented by the formula $\psi$, is a time displaced copy of another phenomenon, represented by the formula $\varphi$, with a maximal time delay $\tau$, i.e., $\psi$ depends always in the positive as well as in the negative case on $\varphi$.
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 \Leftrightarrow_{\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. And conversely, whenever $\varphi$ does continuously not hold for at least $\tau$ time units, then eventually within this time span, $\psi$ is false and remains false at least as long as $\varphi$ does not hold.
Examples
EXAMPLE 1
  FORMAL $\square( \mathit{hazardousCondition} \wedge \mathit{windowOpen} \Leftrightarrow_{\le 30} \mathit{warnedUser})$
  NATURAL
LANGUAGE		 Whenever a window is continuously open during a hazardous condition for at least 30 seconds, then eventually within this time span, a user is warned and remains warned at least as long as this precondition is true. And conversely, whenever a window is closed or there is no hazardous condition for at least 30 time units, then eventually within this time span, the user warning is suppressed and remains suppressed at least as long as this precondition holds.
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 \Leftrightarrow_{\le \tau_1} \varphi_2) \wedge \square( \... ... \rightarrow \square( \varphi_1 \Leftrightarrow_{\le \tau_1+\tau_2} \varphi_3)$
  EXPLANATION This theorem expresses the transitivity of this pattern.
THEOREM 2 Conclusion Distributivity over $\wedge$ (One Direction)
  FORMAL $(\square( \varphi_1 \Leftrightarrow_{\le \tau_1} \psi_1) \wedge \square( \varp... ...arrow \square( \varphi_1 \Leftrightarrow_{\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 in one direction. Note that the other direction is not a valid formula.




 Übergeordnete Seite: Pp

 Feedback
Zu den Kontaktdetails des Verantwortlichen dieser Seite

 English
This page in english. Diese Seite auf englisch.