Invariance

Invariance

Invariance
INTENTION This pattern is applicable if the invariance of a state, represented by $\varphi$, is expressed.
It is intended that $\varphi$ can only be instantiated by a formula containing no temporal operators, because otherwise $\varphi$ does not represent a state.
SIGNATURE $\mathcal{V}^{\mathit{fo}} = \{\varphi\}$, $\mathcal{V}^{\mathit{fu}} = \emptyset$, $\mathcal{V}^{\mathit{te}} = \emptyset$, $\mathcal{V}^{\mathit{ti}} = \emptyset$
FORMAL $\square \varphi$
NATURAL LANGUAGE $\varphi$ is always true.
Examples
EXAMPLE 1
  FORMAL $\square (\mathit{reactionTime} = 11)$
  NATURAL
LANGUAGE		 The reaction time of a sensor, e.g. a temperature sensor, is always 11 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}} = \emptyset$
THEOREM 1 Distributivity of $\square$ over $\wedge$
  FORMAL $\square( \varphi \wedge \psi) \leftrightarrow (\square \varphi ) \wedge (\square \psi )$
  EXPLANATION This theorem expresses the distributivity over $\wedge$ of two instantiations of this pattern.
THEOREM 2 Distributivity of $\square$ over $\vee$ (one direction)
  FORMAL $(\square \varphi ) \vee (\square \psi ) \rightarrow \square( \varphi \vee \psi)$
  EXPLANATION This theorem expresses the distributivity over $\vee$ 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.