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-12 15:54] – [BDD] skrupellos | uni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1 | ||
---|---|---|---|
Line 149: | Line 149: | ||
==== CTL ==== | ==== CTL ==== | ||
- | ^ AG | Auf allen Pfaden gilt immer ... | | + | |
- | ^ EF | Auf einem Pfad gilt irgendwann (für immer???) ... | | + | ^ Propositionale Variablen |
+ | ^ Junktoren | ¬,∧,∨,⇒,⇔ | ::: | | ||
+ | ^ Formel | ϕ,ψ,… | ::: | | ||
+ | ^ Konstanten | ⊤,⊥ | ::: | | ||
+ | ^ Foo | $AX, EX, A[\phi U \psi], E[\phi U \psi], AG \phi, AF \phi, EG \phi, EF \phi$ | | | ||
AG⇔¬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.1405173272.txt.gz · Last modified: 2020-11-18 18:10 (external edit)