Differences

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

--- uni:6:fsv:start [2014-07-13 01:37] – [CTL] skrupellos
+++ uni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1
@@ Line 219: / Line 219: @@
 Zeitkomplexität: Linear zu Transitionen
-Aber //state-explosion-problem//: Exponentiell mit Anzahl zu modelierender Prozesse
+Aber //state-explosion-problem//: Exponentiell mit Anzahl zu modelierender Prozesse \\ => BDDs verhindern das (es kann optimiert werden)
+=== Fairnes ===
+Alle interessierenden Zustände können immer unendlich offt erreicht werden.
+  * D.h. für ''E?'', es Existiert ein fairer Pfad in dem ...
+  * D.h. für ''A?'', in allen fairen Pfaden gild ...
+Abwandlung des Labeling Algorithmuses:
+  * Starke Zusammenhangskomponente ist fair, wenn ein Zustand Fairnesbedingung erfüllt
+  * Zustand ist fair, wenn ein (längerer) Pfad zu fairen starken Zusamenhangskomponente existiert
+=== Encoding of CTL in BDD ===
+BDD ist ein Bitvektor und daher kann ich ein Transitionsystem eincodieren, sowie ein $\phi$.
+http://nicta.com.au/__data/assets/pdf_file/0018/14814/lecture4-mc2.pdf
+<WRAP center round important 60%>
+ToDo
+</WRAP>
+==== LTL ====
+^ Propositionale Variablen | $p, q, \ldots$ | **eingeschränktes** CTL! |
+^ Junktoren | $\neg, \wedge$ | ::: |
+^ Formel | $\phi, \psi, \ldots$ | ::: |
+^ Konstanten | $\top$ | ::: |
+^ Foo | $X \phi, F \phi, G \phi, \phi U \psi$ | |
+  * Fairness direkt angebbar: ''**(GF** p1.state=running**) =>** ...''
+  * CTL ist ausdrucksstärker
+  * Für **alle** Pfade muss ... gelten
+==== Büchi Automat ====
+$(\Sigma, T, I, E, \delta)$
+| $\Sigma$ | Menge | Alphabet |
+| $Z$ | Menge | Zustände |
+| $I$ | Menge | Anfangszustände |
+| $E$ | Menge | Endzustände |
+| $\delta$ | Relation | Zustandsübergänge |
+  * Nichtdeterministisch
+  * Unendliche Wörter
+  * Akzeptiert: Wenn mindestens ein Lauf //existiert//, der immer zu einem Endzustand kommen (unendlich offt)
+$L = (b^{*}a)^\omega$ (wenn ''a'' immer wieder vorkommen muss)
+| $\omega$ | FG | Unendlich offt vorkommen |
+| $*$      | GF | Endlich offt vorkommen   |
+===== Typanalyse =====
+==== While Programm ====
+  * ''**while [**...**] do **...''
+  * ''**if [**...**] then **...** else **...''
+  * ''**true**''
+  * ''**false**''
+  * ''**not **...''
+  * ''... **:= **...''
+  * Aritmetische Ausdrücke
+  * Boolsche Ausdrücke
+==== Datenflussgleichung ====
+"Erreichbare Definitionen" (Reachable Definitions)
+  * $RD_{{\color{ForestGreen}entry}}(\ell) = \bigcup_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}RD_{exit}({\color{red}\ell'})$
+  * $RD_{exit}(\ell) = (RD_{{\color{ForestGreen}entry}}(\ell) \setminus \text{"Entwertete Zuweisungen"}) \cup \text{ "Neue Zuweisungen"}$
+  * 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)$ ^
+| 1 | (x, ?), (y, ?) | ... |
+| 2 | ... | ... |
+| 3 | ... | ... |
+So lange ausfüllen, bis nichts mehr geht.
+Das geht, weil //Fixpunkte// und //Knaster-Tarski-Theorem//
 ==== SMV ====
+Teile
+  - MODULE
+  - VAR
+  - ASSIGN
+  - INIT
+  - TRANS
+  - SPEC
+  - JUSTICE/FAIRNESS
+  * Case sensitive
+  * Wenn uterspezifiziert: Deterministisch
+  * Wenn Block mehrfach: Konjunktion
+  * Nur einzelnes Zeichen: **''&''** bzw. **''|''**
+  * Nur Einfacher Strich: **''%%->%%''** für =>
+  * Negieren, um Lösung als Gegenbeispiel zu bekommen
+=== MODULE ===
 <code>
 MODULE main
+</code>
+-- oder --
+<code>
+MODULE p(x, y, z)
+</code>
+  * Keine Typ angaben
+=== VAR ===
+<code>
 VAR
   a : boolean;
   b : {foo, bar};
+  c : process otherModule(foo, bar);
+</code>
+  * ''... **:** ... **;**''
+  * ''boolean''
+  * Set: ''{}''
------------------------
+=== ASSIGN ===
+<code>
 ASSIGN
-  init(b) := foo
+  init(b) := foo;
-  next(b) := {foo, bar}
+  next(b) := {foo, bar};
   next(b) := case
                foo  : bar;
                TRUE : {foo, bar};
              esac;
--- oder ---------------
+  c := !b
+</code>
+  * ''... **:=** ...**;**''
+  * ''init()''
+  * ''next()''
+  * Invarianten
+  * ''case ... esac''
+  * Ersetzt ''INIT'', ''TRANS'' und ''INVAR''
+Bei ''case'': ''Boolscher Test: Wert/Set;''
+=== INIT ===
+<code>
 INIT
-  b = foo
+  b = foo;
+</code>
+  * ''... **=** ... **;**''
+=== TRANS ===
+<code>
 TRANS
-    b = foo & next(foo) = bar
+    b = foo & next(b) = bar
-  |
+  | b = bar & next(b) = foo
------------------------
+  | b = bar & next(b) = bar
+</code>
+  * Transition, wenn Formel erfüllt
+=== INVAR ===
+<code>
+INVAR
+  Ziege.pos = Wolf.pos -> Bauer.pos = Ziege.pos
+</code>
+  * Invariante
+=== SPEC ===
+<code>
 SPEC
   AG(a -> AF b = foo)
+</code>
+=== DEFINE ===
+<code>
+DEFINE
+  foo := myVar = foo & myOtherVAr = bar;
+</code>
+  * ''... **:=** ... **;**''
+=== JUSTICE/FAIRNESS ===
+<code>
+JUSTICE/FAIRNESS
+  p1.status = running
+</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 ====
+==== Alternating Bit Protocol ====
+  * Zwei Kommunikationspartner
+  * Bidirektionaler Kanal
+  * Nachricht: OK/Defekt
+  * So lange wiederholen bis es klapt
+OK
+^ Kontrollbit: 0 ^ Nachricht | -> ^  | OK |
+^ || <- ^ 0 | ::: |
+^ Kontrollbit: 1 ^ Nachricht | -> ^  | OK |
+^ || <- ^ 1 | ::: |
+Fehler
+^ Kontrollbit: 0 ^ Nachricht | -> ^ ✘ | Fehler beim Empfänger \\ => Unerwartetes Kontrollbit zurück senden |
+^ || <- ^ 1 | ::: |
+^ Kontrollbit: 0 ^ Nachricht | -> ^  | Fehler beim Sender |
+^ ✘ || <- ^ 0 | ::: |
+^ Kontrollbit: 0 ^ Nachricht | -> ^  | OK |
+^ || <- ^ 0 | ::: |
+^ Kontrollbit: 1 ^ Nachricht | -> ^ ✘ | Fehler beim Empfänger \\ => Unerwartetes Kontrollbit zurück senden |
+^ || <- ^ 0 | ::: |
+^ Kontrollbit: 1 ^ Nachricht | -> ^  | Fehler beim Sender |
+^ ✘ || <- ^ 1 | ::: |
+^ Kontrollbit: 1 ^ Nachricht | -> ^  | OK |
+^ || <- ^ 1 | ::: |