LimitedInvariance

Limited Invariance

Limited Invariance
INTENTION This pattern is applicable if the fluttering of a phenomenon is suppressed, i.e., if a phenomenon, represented by $\varphi$, reaches a specific state, it remains in this state for at least $\tau$ time units.
SIGNATURE $\mathcal{V}^{\mathit{fo}} = \{\varphi\}$, $\mathcal{V}^{\mathit{fu}} = \emptyset$, $\mathcal{V}^{\mathit{te}} = \emptyset$, $\mathcal{V}^{\mathit{ti}} = \{\tau\}$
FORMAL $\square(\bigtriangledown\limits_{\leq \tau} \varphi)$
NATURAL LANGUAGE Whenever $\varphi$ becomes true, it remains true for at least $\tau$ time units.
Examples
EXAMPLE 1
  FORMAL $\square(\bigtriangledown\limits_{\leq \mathit{T\_MinInf}} (\mathit{indicatorLight} = 1))$
  NATURAL
LANGUAGE		 Whenever an indicator light is switched on, it remains for at least T_MinInf time units.
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\}$
THEOREM 1 Expansion of $\bigtriangledown$ over $\wedge$
  FORMAL $\square( \bigtriangledown\limits_{\le \tau} (\varphi \wedge \psi)) \rightarrow ... ...edown\limits_{\le \tau} \varphi \vee \bigtriangledown\limits_{\le \tau} \psi )$
  EXPLANATION This theorem expresses how a conjunctive combination of two phenomena can be expanded.
THEOREM 2 Contraction of $\bigtriangledown$ over $\wedge$
  FORMAL $\square( \bigtriangledown\limits_{\le \tau} \varphi) \wedge \square( \bigtrian... ...) \rightarrow \square( \bigtriangledown\limits_{\le \tau} (\varphi \vee \psi))$
  EXPLANATION This theorem expresses how a conjunctive combination of two instantiations of this pattern can be contracted.




 Übergeordnete Seite: Pp

 Feedback
Zu den Kontaktdetails des Verantwortlichen dieser Seite

 English
This page in english. Diese Seite auf englisch.