Differences

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

--- uni:6:fsv:start [2014-07-08 22:07] – skrupellos
+++ uni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1
@@ Line 35: / Line 35: @@
 ==== Tseitin Übersetzung ====
+**Nur erfüllungsäquivalent**
   * Rekursive Funktion //KNF//
+    * Rein
+      * (Nicht-Normalisierte) Formel
+    * Raus
+      * Neuster (frischer) Variablenname
+      * KNF
   * //C// ist frische Variable
   * Regel:  $C \Leftrightarrow \phi$  als KNF
@@ Line 49: / Line 56: @@
 ==== SAT-Solver ====
 SAT
-  * //"ist  $\phi$  erfüllbar?"//
+  * //"ist // $\phi$ // erfüllbar?"//
   * Entscheidungsproblem (NP-Hart)
   * **Nur für KNF**
@@ Line 56: / Line 63: @@
   * Erweiterung auf Äquivalenz von  $\phi$  und  $\psi$ :  $\neg (\phi \Leftrightarrow \psi)$  unerfüllbar?
+==== DPLL-Algorithmus ====
+  * Rekursive Funktion DPLL
+    * Rein
+      * (Teil) Besetzung
+      * (Rest) KNF
+    * Raus
+      * Bessere Belegung
+<WRAP center round important 60%>
+Hier gibt es mehr. Aber das halte ich für Klausurirrelevant
+</WRAP>
+==== Gleichheit von Schaltkreisen ====
+Wenn gezeigt werden soll, das die Schaltungen  $f$  und  $f'$  bezüglich ihrer Eingänge  $x\ldots$  das selbe liefern, dann darf
+ $\neg \left( \left(f_1(x\ldots) \Leftrightarrow f'_1(x\ldots)\right) \wedge \left(f_2(x\ldots) \Leftrightarrow f'_2(x\ldots)\right)\right)$
+//keine Lösung// liefern.
+==== Nebenläufige Systeme ====
+^ ^^ Zeit ^^^^
+^ ::: ^^ 0 ^ 1 ^ ... ^ n-1 ^
+^Zustand ^  $z_1$  |  $x_{zt}$  | | |
+^:::^  $z_2$  |   | | |
+^:::^ ... |   | | |
+|  $\bigwedge_t \bigwedge_{z \in Z} \bigwedge_{z' \ne z}\neg(x_{zt} \wedge x_{z't})$  | Zu //jeder Zeit// ist nur ein zustand gesetzt |
+|  $\bigvee_{z \in I} x_{z0}$  | //Einer der Startzustände// |
+|  $\bigwedge^{n-2}_{t=0} \bigvee_{z \rightarrow z'} x_{zt} \wedge x_{z'(t+1)}$  | Zu //jeder Zeit// führt ein Zustand in //einen Folgezustand// |
+|  $\bigvee^{n-1}_{t=0} \bigvee_{z \in V} x_{zt}$  | Zu //einer Zeit// ist //ein verbotener Zustand// erreicht|
+Dieses System darf keine Lösung haben.
+==== BDD ====
+nichtreduzierter BDDs
+  * Gerichtet
+  * Azyklisch
+  * Knoten auf Pfad mit //fixer Ordnung// (es dürfen welche fehlen)
+reduzierte BDDs (zusätzlich)
+  * Keine Kanten mit identischen Start und Ziel (gleich ist OK)
+  * Keine Redundanz (isomarphen Teilgraphen)
+  * Nur //True// und //False// als Blätter (jeweils max. 1x)
+nichtreduziert -> reduziert
+  * Knoten mit identischen Nachfolgern entfernen
+  * Knoten: Name gleich & Nachfolger gleich => verschmelzen
+  * //True//%%/%%//False// verschmelzen.
+BDDs sind //eindeutig//: Gleiche Funktion => isomorphe BDDs
+Shannon-Zerlegung:  $f = (x \wedge f[x := \top]) \vee (\neg x \wedge f[x := \perp])$
+Negation: //True// und //False// vertauschen
+Variable setzen:
+  - ersetzen/umlenken
+  - reduzieren
+Zweistellige Operationen: Rekursiv  $(x \wedge (f[x := \top] \oplus g[x := \top])) \vee (\neg x (\wedge f[X := \perp] \oplus g[x := \perp]))$
+(Gehe die Variablen der reihe nach durch. Ersetze die Nachfolger durch  $\oplus$  aus den //True//-Zweigen und durch  $\oplus$  aus den //False//-Zweigen.)
+Alle möglichkeiten einer Variablen probieren:  $\exists x: f := f[x := \top] \vee f[x :=\perp]$
+Optiomierungen
+  * Umordnen (extremfall: explonential)
+  * Teilographen wiederverwenden (Hash-Funktion zum finden)
+<WRAP center round important 60%>
+Es fehlen nebenläufige Systeme!!!
+</WRAP>
+===== Model checking =====
+Arten
+  * Bounded (Beschränkt durch die Symulationszeit)
+    * SAT Solver
+  * Symbolic
+    * BDDs
+Dinge die Interessieren
+  * Safty: Keine verbotenen Zustände erreichbar
+  * Liveness: Reset-Zustand immer erreichbar? Kein verklemmen  $AG(EF\bigwedge_p q_{p,sleep})$
+  * Fairness: "Gute Eigenschaft" gilt für alle fairen Abläufe
+==== CTL ====
+^ Propositionale Variablen |  $p, q, \ldots$  | Jedes Aussgenlogische Formel ist CTL! |
+^ Junktoren |  $\neg, \wedge, \vee, \Rightarrow, \Leftrightarrow$  | ::: |
+^ Formel |  $\phi, \psi, \ldots$  | ::: |
+^ Konstanten |  $\top, \perp$  | ::: |
+^ Foo |  $AX, EX, A[\phi U \psi], E[\phi U \psi], AG \phi, AF \phi, EG \phi, EF \phi$  | |
+ $AG \Leftrightarrow \neg EF(\neg \phi)$
+<WRAP second column>
+^A|Auf allen Pfaden gilt ...|
+^E|Auf (mindestens) einem Pfad gilt ...|
+</WRAP>
+<WRAP second column>
+...in...
+</WRAP>
+<WRAP second column>
+^X|Ne**x**t|... (mindestens) einem unmittelbar folgenden Zustand|
+^F|**F**inal|... (mindestens) einem folgenden/selben Zustand|
+^G|**G**lobaly|... allen folgenden/selben Zuständen|
+^U|**U**ntil|... allen folgenden/selben Zuständen  $\phi$ , bis  $\psi$  gilt. \\  $\psi$  kann bereits im selben gelten|
+</WRAP>
+=== Transitinssystem ===
+ $(S, \rightarrow)$
+  * Zustands//menge//:  $\{(False, True), (True, False), (True, True)\}$
+  * Transitionsrealtion:  $\{\left(\left(Fals, True\right), \left(True, False\right)\right), \ldots\}$
+===Interpretationen===
+^  $Tr(\mathcal{I})$  |  $(S, \rightarrow)$  | Transitionsystem | Durch  $\mathcal{I}$  festgelegt |
+^  $\mathcal{I}(p)$   |  $\subseteq S$  | Zustände in denen  $p$  gilt | ::: |
+^  $s \models \mathcal{I} p$  |  $\{True, False\}$  | Aussage:  $p$  ist in Zustand  $s$  gesetzt | ::: |
+^  $\mathcal{I}(\phi)$   |  $\subseteq S$  | Zustände in denen  $\phi$  gilt | Ableitbar |
+^  $s \models \mathcal{I} \phi$  |  $\{True, False\}$  | Aussage:  $\phi$  ist in Zustand  $s$  gesetzt | ::: |
+Interpretation enthält keine Formel.
+===Äquivalenz ===
+  * (AE)(GF) vertauschen und 2xnegieren
+    *  $AG(\phi) \Longleftrightarrow \neg EF(\neg \phi)$
+    *  $AF(\phi) \Longleftrightarrow \neg EG(\neg \phi)$
+    *  $EF(\phi) \Longleftrightarrow \neg AG(\neg \phi)$
+    *  $EG(\phi) \Longleftrightarrow \neg AF(\neg \phi)$
+  *  $AG(\phi \wedge \psi) \Longleftrightarrow AG(\phi) \wedge AG(\psi)$
+  *  $AF(\phi) \Longleftrightarrow A[\top U \phi]$
+  *  $EF(\phi) \Longleftrightarrow E[\top U \phi]$
+  *  $A\[\phi U \psi\] \Longleftrightarrow \neg (E[\neg \phi U (\neg \phi \wedge \neg \psi)] \vee EG(\neg \phi))$
+=== Labeling Algorithmus ===
+  - Formel umformen (nur noch  $\neg, \wedge, \perp, AF, E[\cdot U \cdot ]$ )
+  - Teilformeln bis auf Variablen-Ebene finden
+  - Teilformeln Bottom-up durchgehen, bis nichts mehr geht
+    - Graph mit geltenden Teilformeln markieren, bis nichts mehr geht (dabei auf bereits markiertes berufen)
+Markiere mit ..
+  *  $AF(\phi)$ , wo ..
+    *  $\phi$
+    * Alle Nachfolger sind  $AF(\phi)$
+  *  $E[\phi U \psi]$ , wo ..
+    *  $\psi$
+    *  $\phi$  und Folgezustand mit  $E[\phi U \psi]$
+Effizienter:  $EG(\phi)$  anstatt  $AF(\phi)$
+  -  $\neg\phi$  für Ausblenden/Ignorieren/Streichen
+  - Starke Zusammenhangskomponenten markieren (Ring-Pfad durch Knoten)
+  - Markiere Knoten, die in eine  //echte// starke Zusammenhangskomponenten zeigen
+Zeitkomplexität: Linear zu Transitionen
+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;
+  next(b) := {foo, bar};
+  next(b) := case
+               foo  : bar;
+               TRUE : {foo, bar};
+             esac;
+  c := !b
+</code>
+  * ''... **:=** ...**;**''
+  * ''init()''
+  * ''next()''
+  * Invarianten
+  * ''case ... esac''
+  * Ersetzt ''INIT'', ''TRANS'' und ''INVAR''
+Bei ''case'': ''Boolscher Test: Wert/Set;''
+=== INIT ===
+<code>
+INIT
+  b = foo;
+</code>
+  * ''... **=** ... **;**''
+=== TRANS ===
+<code>
+TRANS
+    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 | ::: |