Differences

This shows you the differences between two versions of the page.

--- uni:6:fsv:start [2014-07-15 15:30] – [CTL] skrupellos
+++ uni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1
@@ Line 249: / Line 249: @@
   * Fairness direkt angebbar: ''**(GF** p1.state=running**) =>** ...''
   * CTL ist ausdrucksstärker
+  * Für **alle** Pfade muss ... gelten
 ==== Büchi Automat ====
@@ Line 280: / Line 281: @@
 ==== Datenflussgleichung ====
-"Reichweite von Zuweisungen"
+"Erreichbare Definitionen" (Reachable Definitions)
-  * $RD_{exit}(\ell) = (RD_{exit}(\ell) \setminus \text{"Entwertete Zuweisungen"}) \cup \text{ "Neue Zuweisungen"}$
+  * $RD_{{\color{ForestGreen}entry}}(\ell) = \bigcup_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}RD_{exit}({\color{red}\ell'})$
-  * $RD_{entry}(\ell) = \bigcup_{\ell':\ell'\rightarrow\ell}RD_{exit}(\ell')$
+  * $RD_{exit}(\ell) = (RD_{{\color{ForestGreen}entry}}(\ell) \setminus \text{"Entwertete Zuweisungen"}) \cup \text{ "Neue Zuweisungen"}$
-  * Zu beginn werden //alle// Variablen mit "(X, ?)" initialisiert.
+  * Zu beginn werden //alle// Variablen mit "$(X, \ell)$" initialisiert.
+"Verfügbare Ausdrücke" (Available Expressions)
+  * $AE_{{\color{ForestGreen}entry}}(\ell) = {\color{blue}\bigcap}_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}AE_{exit}({\color{red}\ell'})$
+  * $AE_{exit}(\ell) = (AE_{{\color{ForestGreen}entry}}(\ell) \setminus kill_{AE}(B^\ell)) \cup gen_{AE}(B^\ell)$
+  * $kill_{AE}([x:=a]^\ell) = \{\text{Formeln, die }x\text{ enthalten}\}$
+  * $gen_{AE}([x := a]) = \{\text{Teilausdrücke von }a\text{ ohne }x\}$
+  * $gen_{AE}([bool\ exp]) = \{\text{Teilausdrücke von }bool\ exp\}$
+  * Zu beginn werden //alle// Variablen mit "$\emptyset$" initialisiert.
+  * //Nur// Arithmetische Ausdrücke
+"Lebendige Variablen" (Live Variables)
+  * $LV_{exit}(\ell) = \bigcup_{{\color{red}\ell'}:\ell\rightarrow{\color{red}\ell'}}LV_{{\color{ForestGreen}entry}}({\color{red}\ell'})$
+  * $LV_{{\color{ForestGreen}entry}}(\ell) = (LV_{exit}(\ell) \setminus kill_{LV}(B^\ell)) \cup gen_{LV}(B^\ell)$
+  * $kill_{LV}([x:=a]^\ell) = \{x\}$
+  * $gen_{LV}([x := a]) = \{\text{Variablen in }a\}$
+  * $gen_{LV}([bool\ exp]) = \{\text{Variablen in }bool\ exp\}$
+  * Zu beginn werden //alle// Variablen mit "$\emptyset$" initialisiert.
 ^ $\ell$ ^ $RD_{entry}(\ell)$ ^ $RD_{exit}(\ell)$ ^
@@ Line 291: / Line 312: @@
 | 3 | ... | ... |
+So lange ausfüllen, bis nichts mehr geht.
+Das geht, weil //Fixpunkte// und //Knaster-Tarski-Theorem//
 ==== SMV ====
 Teile
@@ Line 392: / Line 416: @@
 </code>
+===== Beweise =====
+==== Vollständiger Verband ====
+Verband $(L, \sqsubseteq)$
+  * **reflexiv** \\ $\forall_{x \in L} : x \sqsubseteq x$
+  * **transitiv** \\ $\forall_{x, y, z \in L} : x \sqsubseteq y \wedge y \sqsubseteq z \Rightarrow x \sqsubseteq z$
+  * **antisymetrisch** \\ $\forall_{x, y \in L} : x \sqsubseteq y \wedge y \sqsubseteq x \Rightarrow x = y$
+  * **Jede Teilmenge hat ein Supremum** \\ Jedes $U \subseteq L$ hat ein $\bigsqcup U$
+==== Supremum ====
+$s = \bigsqcup U$
+  * **Ist obere Schranke** \\ $\forall_{x \in U} : x \sqsubseteq s$
+  * **Ist //kleinste// obere Schranke** \\ $s' \text{ ist obere Schranke } \Rightarrow s \sqsubseteq s'$
+==== Monotonie ====
+  * $x \sqsubseteq y \Rightarrow F(x) \sqsubseteq F(y)$
+==== Fixpunkt ====
+  * $\exists x: F(x) = x$
+Dazu muss $F(x)$ monoton sein.
 ===== Probleme =====
 ==== Semaphor ====