Loading [MathJax]/jax/output/CommonHTML/jax.js

Wiki

A universe of ideas

User Tools

Site Tools


uni:6:fsv:start

Differences

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

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision
Previous revision
uni:6:fsv:start [2014-07-08 22:07] skrupellosuni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1
Line 35: Line 35:
  
 ==== Tseitin Übersetzung ==== ==== Tseitin Übersetzung ====
 +**Nur erfüllungsäquivalent**
 +
   * Rekursive Funktion //KNF//   * Rekursive Funktion //KNF//
 +    * Rein
 +      * (Nicht-Normalisierte) Formel
 +    * Raus
 +      * Neuster (frischer) Variablenname
 +      * KNF
   * //C// ist frische Variable   * //C// ist frische Variable
   * Regel: Cϕ als KNF   * Regel: Cϕ als KNF
Line 49: Line 56:
 ==== SAT-Solver ==== ==== SAT-Solver ====
 SAT SAT
-  * //"ist ϕ erfüllbar?"//+  * //"ist //ϕ// erfüllbar?"//
   * Entscheidungsproblem (NP-Hart)   * Entscheidungsproblem (NP-Hart)
   * **Nur für KNF**   * **Nur für KNF**
Line 56: Line 63:
   * Erweiterung auf Äquivalenz von ϕ und ψ: ¬(ϕψ) unerfüllbar?   * Erweiterung auf Äquivalenz von ϕ und ψ: ¬(ϕψ) 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 das selbe liefern, dann darf
 +¬((f1(x)f1(x))(f2(x)f2(x)))
 +//keine Lösung// liefern.
 +
 +==== Nebenläufige Systeme ====
 +^ ^^ Zeit ^^^^
 +^ ::: ^^ 0 ^ 1 ^ ... ^ n-1 ^
 +^Zustand ^ z1 | xzt | | |
 +^:::^ z2 |   | | |
 +^:::^ ... |   | | |
 +
 +| tzZzz¬(xztxzt) | Zu //jeder Zeit// ist nur ein zustand gesetzt |
 +| zIxz0 | //Einer der Startzustände// |
 +| n2t=0zzxztxz(t+1) | Zu //jeder Zeit// führt ein Zustand in //einen Folgezustand// |
 +| n1t=0zVxzt | 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=(xf[x:=])(¬xf[x:=⊥])
 +
 +Negation: //True// und //False// vertauschen
 +
 +Variable setzen:
 +  - ersetzen/umlenken
 +  - reduzieren
 +
 +Zweistellige Operationen: Rekursiv (x(f[x:=]g[x:=]))(¬x(f[X:=⊥]g[x:=⊥]))
 +(Gehe die Variablen der reihe nach durch. Ersetze die Nachfolger durch aus den //True//-Zweigen und durch aus den //False//-Zweigen.)
 +
 +Alle möglichkeiten einer Variablen probieren: x:f:=f[x:=]f[x:=⊥]
 +
 +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(EFpqp,sleep)
 +  * Fairness: "Gute Eigenschaft" gilt für alle fairen Abläufe
 +
 +==== CTL ====
 +
 +^ Propositionale Variablen | p,q, | Jedes Aussgenlogische Formel ist CTL! |
 +^ Junktoren | ¬,,,, | ::: |
 +^ Formel | ϕ,ψ, | ::: |
 +^ Konstanten | , | ::: |
 +^ Foo | AX,EX,A[ϕUψ],E[ϕUψ],AGϕ,AFϕ,EGϕ,EFϕ | |
 +
 +
 +AG¬EF(¬ϕ)
 +<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 ϕ, bis ψ gilt. \\ ψ kann bereits im selben gelten|
 +</WRAP>
 +
 +=== Transitinssystem ===
 +(S,)
 +
 +  * Zustands//menge//: {(False,True),(True,False),(True,True)}
 +  * Transitionsrealtion: {((Fals,True),(True,False)),}
 +
 +===Interpretationen===
 +^ Tr(I) | (S,) | Transitionsystem | Durch I festgelegt |
 +^ I(p)  | S | Zustände in denen p gilt | ::: |
 +^ sIp | {True,False} | Aussage: p ist in Zustand s gesetzt | ::: |
 +^ I(ϕ)  | S | Zustände in denen ϕ gilt | Ableitbar |
 +^ sIϕ | {True,False} | Aussage: ϕ ist in Zustand s gesetzt | ::: |
 +
 +Interpretation enthält keine Formel.
 +
 +===Äquivalenz ===
 +  * (AE)(GF) vertauschen und 2xnegieren
 +    * AG(ϕ)¬EF(¬ϕ)
 +    * AF(ϕ)¬EG(¬ϕ)
 +    * EF(ϕ)¬AG(¬ϕ)
 +    * EG(ϕ)¬AF(¬ϕ)
 +  * AG(ϕψ)AG(ϕ)AG(ψ)
 +  * AF(ϕ)A[Uϕ]
 +  * EF(ϕ)E[Uϕ]
 +  * A\[ϕUψ\]¬(E[¬ϕU(¬ϕ¬ψ)]EG(¬ϕ))
 +
 +=== Labeling Algorithmus ===
 +  - Formel umformen (nur noch ¬,,,AF,E[U])
 +  - 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(ϕ), wo ..
 +    * ϕ
 +    * Alle Nachfolger sind AF(ϕ)
 +  * E[ϕUψ], wo ..
 +    * ψ
 +    * ϕ und Folgezustand mit E[ϕUψ]
 +
 +Effizienter: EG(ϕ) anstatt AF(ϕ)
 +  - ¬ϕ 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 ϕ.
 +
 +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, | **eingeschränktes** CTL! |
 +^ Junktoren | ¬, | ::: |
 +^ Formel | ϕ,ψ, | ::: |
 +^ Konstanten | | ::: |
 +^ Foo | Xϕ,Fϕ,Gϕ,ϕUψ | |
 +
 +  * Fairness direkt angebbar: ''**(GF** p1.state=running**) =>** ...''
 +  * CTL ist ausdrucksstärker
 +  * Für **alle** Pfade muss ... gelten
 +
 +==== Büchi Automat ====
 +(Σ,T,I,E,δ)
 +
 +| Σ | Menge | Alphabet |
 +| Z | Menge | Zustände |
 +| I | Menge | Anfangszustände |
 +| E | Menge | Endzustände |
 +| δ | Relation | Zustandsübergänge |
 +
 +  * Nichtdeterministisch
 +  * Unendliche Wörter
 +  * Akzeptiert: Wenn mindestens ein Lauf //existiert//, der immer zu einem Endzustand kommen (unendlich offt)
 +
 +L=(ba)ω (wenn ''a'' immer wieder vorkommen muss)
 +
 +| ω | 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)
 +
 +  * RDentry()=:RDexit()
 +  * RDexit()=(RDentry()"Entwertete Zuweisungen") "Neue Zuweisungen"
 +  * Zu beginn werden //alle// Variablen mit "(X,)" initialisiert.
 +
 +
 +
 +"Verfügbare Ausdrücke" (Available Expressions)
 +  * AEentry()=:AEexit()
 +  * AEexit()=(AEentry()killAE(B))genAE(B)
 +  * killAE([x:=a])={Formeln, die x enthalten}
 +  * genAE([x:=a])={Teilausdrücke von a ohne x}
 +  * genAE([bool exp])={Teilausdrücke von bool exp}
 +  * Zu beginn werden //alle// Variablen mit "" initialisiert.
 +  * //Nur// Arithmetische Ausdrücke
 +
 +
 +"Lebendige Variablen" (Live Variables)
 +  * LVexit()=:LVentry()
 +  * LVentry()=(LVexit()killLV(B))genLV(B)
 +  * killLV([x:=a])={x}
 +  * genLV([x:=a])={Variablen in a}
 +  * genLV([bool exp])={Variablen in bool exp}
 +  * Zu beginn werden //alle// Variablen mit "" initialisiert.
 +
 +^ ^ RDentry() ^ RDexit() ^
 +| 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,)
 +  * **reflexiv** \\ xL:xx
 +  * **transitiv** \\ x,y,zL:xyyzxz
 +  * **antisymetrisch** \\ x,yL:xyyxx=y
 +  * **Jede Teilmenge hat ein Supremum** \\ Jedes UL hat ein U
 +
 +==== Supremum ====
 +s=U
 +
 +  * **Ist obere Schranke** \\ xU:xs
 +  * **Ist //kleinste// obere Schranke** \\ s ist obere Schranke ss
 +
 +==== Monotonie ====
 +  * xyF(x)F(y)
 + 
 +==== Fixpunkt ====
 +  * 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 | ::: |
uni/6/fsv/start.1404850058.txt.gz · Last modified: 2020-11-18 18:10 (external edit)