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.





 

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

 
This page in german. Diese Seite auf deutsch.