uni:6:fsv:start
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
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 ==== | ==== 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?"// | + | * //" |
* 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 | ||
+ | </ | ||
+ | |||
+ | ==== 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…)⇔f′1(x…))∧(f2(x…)⇔f′2(x…))) | ||
+ | //keine Lösung// liefern. | ||
+ | |||
+ | ==== Nebenläufige Systeme ==== | ||
+ | ^ ^^ Zeit ^^^^ | ||
+ | ^ ::: ^^ 0 ^ 1 ^ ... ^ n-1 ^ | ||
+ | ^Zustand ^ z1 | xzt | | | | ||
+ | ^:::^ z2 | | | | | ||
+ | ^:::^ ... | | | | | ||
+ | |||
+ | | ⋀t⋀z∈Z⋀z′≠z¬(xzt∧xz′t) | Zu //jeder Zeit// ist nur ein zustand gesetzt | | ||
+ | | ⋁z∈Ixz0 | //Einer der Startzustände// | ||
+ | | ⋀n−2t=0⋁z→z′xzt∧xz′(t+1) | Zu //jeder Zeit// führt ein Zustand in //einen Folgezustand// | ||
+ | | ⋁n−1t=0⋁z∈Vxzt | 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 | ||
+ | * // | ||
+ | |||
+ | BDDs sind // | ||
+ | |||
+ | Shannon-Zerlegung: | ||
+ | |||
+ | Negation: //True// und //False// vertauschen | ||
+ | |||
+ | Variable setzen: | ||
+ | - ersetzen/ | ||
+ | - reduzieren | ||
+ | |||
+ | Zweistellige Operationen: | ||
+ | (Gehe die Variablen der reihe nach durch. Ersetze die Nachfolger durch ⊕ aus den // | ||
+ | |||
+ | Alle möglichkeiten einer Variablen probieren: ∃x:f:=f[x:=⊤]∨f[x:=⊥] | ||
+ | |||
+ | Optiomierungen | ||
+ | * Umordnen (extremfall: | ||
+ | * Teilographen wiederverwenden (Hash-Funktion zum finden) | ||
+ | |||
+ | <WRAP center round important 60%> | ||
+ | Es fehlen nebenläufige Systeme!!! | ||
+ | </ | ||
+ | |||
+ | ===== 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⋀pqp,sleep) | ||
+ | * Fairness: "Gute Eigenschaft" | ||
+ | |||
+ | ==== 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 second column> | ||
+ | ...in... | ||
+ | </ | ||
+ | <WRAP second column> | ||
+ | ^X|Ne**x**t|... (mindestens) einem unmittelbar folgenden Zustand| | ||
+ | ^F|**F**inal|... (mindestens) einem folgenden/ | ||
+ | ^G|**G**lobaly|... allen folgenden/ | ||
+ | ^U|**U**ntil|... allen folgenden/ | ||
+ | </ | ||
+ | |||
+ | === Transitinssystem === | ||
+ | (S,→) | ||
+ | |||
+ | * Zustands// | ||
+ | * Transitionsrealtion: | ||
+ | |||
+ | ===Interpretationen=== | ||
+ | ^ Tr(I) | (S,→) | Transitionsystem | Durch I festgelegt | | ||
+ | ^ I(p) | ||
+ | ^ s⊨Ip | {True,False} | Aussage: p ist in Zustand s gesetzt | ::: | | ||
+ | ^ I(ϕ) | ||
+ | ^ s⊨Iϕ | {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: | ||
+ | - ¬ϕ für Ausblenden/ | ||
+ | - Starke Zusammenhangskomponenten markieren (Ring-Pfad durch Knoten) | ||
+ | - Markiere Knoten, die in eine //echte// starke Zusammenhangskomponenten zeigen | ||
+ | |||
+ | Zeitkomplexität: | ||
+ | |||
+ | Aber // | ||
+ | |||
+ | === Fairnes === | ||
+ | Alle interessierenden Zustände können immer unendlich offt erreicht werden. | ||
+ | |||
+ | * D.h. für '' | ||
+ | * D.h. für '' | ||
+ | |||
+ | 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, | ||
+ | |||
+ | http:// | ||
+ | |||
+ | <WRAP center round important 60%> | ||
+ | ToDo | ||
+ | </ | ||
+ | |||
+ | ==== LTL ==== | ||
+ | ^ Propositionale Variablen | p,q,… | **eingeschränktes** CTL! | | ||
+ | ^ Junktoren | ¬,∧ | ::: | | ||
+ | ^ Formel | ϕ,ψ,… | ::: | | ||
+ | ^ Konstanten | ⊤ | ::: | | ||
+ | ^ Foo | Xϕ,Fϕ,Gϕ,ϕUψ | | | ||
+ | |||
+ | * Fairness direkt angebbar: '' | ||
+ | * 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 // | ||
+ | |||
+ | L=(b∗a)ω (wenn '' | ||
+ | |||
+ | | ω | FG | Unendlich offt vorkommen | | ||
+ | | ∗ | GF | Endlich offt vorkommen | ||
+ | |||
+ | ===== Typanalyse ===== | ||
+ | ==== While Programm ==== | ||
+ | * '' | ||
+ | * '' | ||
+ | * '' | ||
+ | * '' | ||
+ | * '' | ||
+ | * '' | ||
+ | * Aritmetische Ausdrücke | ||
+ | * Boolsche Ausdrücke | ||
+ | |||
+ | ==== Datenflussgleichung ==== | ||
+ | " | ||
+ | |||
+ | * RDentry(ℓ)=⋃ℓ′:ℓ′→ℓRDexit(ℓ′) | ||
+ | * RDexit(ℓ)=(RDentry(ℓ)∖"Entwertete Zuweisungen")∪ "Neue Zuweisungen" | ||
+ | * Zu beginn werden //alle// Variablen mit "(X,ℓ)" | ||
+ | |||
+ | |||
+ | |||
+ | " | ||
+ | * 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 " | ||
+ | * //Nur// Arithmetische Ausdrücke | ||
+ | |||
+ | |||
+ | " | ||
+ | * 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 " | ||
+ | |||
+ | ^ ℓ ^ RDentry(ℓ) ^ RDexit(ℓ) ^ | ||
+ | | 1 | (x, ?), (y, ?) | ... | | ||
+ | | 2 | ... | ... | | ||
+ | | 3 | ... | ... | | ||
+ | |||
+ | So lange ausfüllen, bis nichts mehr geht. | ||
+ | |||
+ | Das geht, weil // | ||
+ | ==== SMV ==== | ||
+ | Teile | ||
+ | - MODULE | ||
+ | - VAR | ||
+ | - ASSIGN | ||
+ | - INIT | ||
+ | - TRANS | ||
+ | - SPEC | ||
+ | - JUSTICE/ | ||
+ | |||
+ | * Case sensitive | ||
+ | * Wenn uterspezifiziert: | ||
+ | * Wenn Block mehrfach: Konjunktion | ||
+ | * Nur einzelnes Zeichen: **''&'' | ||
+ | * Nur Einfacher Strich: **'' | ||
+ | * Negieren, um Lösung als Gegenbeispiel zu bekommen | ||
+ | |||
+ | === MODULE === | ||
+ | < | ||
+ | MODULE main | ||
+ | </ | ||
+ | -- oder -- | ||
+ | < | ||
+ | MODULE p(x, y, z) | ||
+ | </ | ||
+ | * Keine Typ angaben | ||
+ | |||
+ | === VAR === | ||
+ | < | ||
+ | VAR | ||
+ | a : boolean; | ||
+ | b : {foo, bar}; | ||
+ | c : process otherModule(foo, | ||
+ | </ | ||
+ | * '' | ||
+ | * '' | ||
+ | * Set: '' | ||
+ | |||
+ | === ASSIGN === | ||
+ | < | ||
+ | ASSIGN | ||
+ | init(b) := foo; | ||
+ | next(b) := {foo, bar}; | ||
+ | next(b) := case | ||
+ | | ||
+ | TRUE : {foo, bar}; | ||
+ | esac; | ||
+ | c := !b | ||
+ | </ | ||
+ | * '' | ||
+ | * '' | ||
+ | * '' | ||
+ | * Invarianten | ||
+ | * '' | ||
+ | * Ersetzt '' | ||
+ | |||
+ | Bei '' | ||
+ | |||
+ | === INIT === | ||
+ | < | ||
+ | INIT | ||
+ | b = foo; | ||
+ | </ | ||
+ | * '' | ||
+ | |||
+ | === TRANS === | ||
+ | < | ||
+ | TRANS | ||
+ | b = foo & next(b) = bar | ||
+ | | b = bar & next(b) = foo | ||
+ | | b = bar & next(b) = bar | ||
+ | </ | ||
+ | |||
+ | * Transition, wenn Formel erfüllt | ||
+ | |||
+ | === INVAR === | ||
+ | < | ||
+ | INVAR | ||
+ | Ziege.pos = Wolf.pos -> Bauer.pos = Ziege.pos | ||
+ | </ | ||
+ | * Invariante | ||
+ | |||
+ | === SPEC === | ||
+ | < | ||
+ | SPEC | ||
+ | AG(a -> AF b = foo) | ||
+ | </ | ||
+ | |||
+ | === DEFINE === | ||
+ | < | ||
+ | DEFINE | ||
+ | foo := myVar = foo & myOtherVAr = bar; | ||
+ | </ | ||
+ | |||
+ | * '' | ||
+ | === JUSTICE/ | ||
+ | < | ||
+ | JUSTICE/ | ||
+ | p1.status = running | ||
+ | </ | ||
+ | |||
+ | ===== Beweise ===== | ||
+ | ==== Vollständiger Verband ==== | ||
+ | Verband (L,⊑) | ||
+ | * **reflexiv** \\ ∀x∈L:x⊑x | ||
+ | * **transitiv** \\ ∀x,y,z∈L:x⊑y∧y⊑z⇒x⊑z | ||
+ | * **antisymetrisch** \\ ∀x,y∈L:x⊑y∧y⊑x⇒x=y | ||
+ | * **Jede Teilmenge hat ein Supremum** \\ Jedes U⊆L hat ein ⨆U | ||
+ | |||
+ | ==== Supremum ==== | ||
+ | s=⨆U | ||
+ | |||
+ | * **Ist obere Schranke** \\ ∀x∈U:x⊑s | ||
+ | * **Ist // | ||
+ | |||
+ | ==== Monotonie ==== | ||
+ | * x⊑y⇒F(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 | ::: | | ||
+ | ^ Kontrollbit: | ||
+ | ^ || <- ^ 1 | ::: | | ||
+ | |||
+ | Fehler | ||
+ | ^ Kontrollbit: | ||
+ | ^ || <- ^ 1 | ::: | | ||
+ | ^ Kontrollbit: | ||
+ | ^ ✘ || <- ^ 0 | ::: | | ||
+ | ^ Kontrollbit: | ||
+ | ^ || <- ^ 0 | ::: | | ||
+ | ^ Kontrollbit: | ||
+ | ^ || <- ^ 0 | ::: | | ||
+ | ^ Kontrollbit: | ||
+ | ^ ✘ || <- ^ 1 | ::: | | ||
+ | ^ Kontrollbit: | ||
+ | ^ || <- ^ 1 | ::: | |
uni/6/fsv/start.1404850058.txt.gz · Last modified: 2020-11-18 18:10 (external edit)