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-13 16:27] – [SMV] skrupellos | uni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1 | ||
---|---|---|---|
Line 219: | Line 219: | ||
Zeitkomplexität: | Zeitkomplexität: | ||
- | Aber // | + | 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 ==== | ==== SMV ==== | ||
Teile | Teile | ||
Line 229: | Line 323: | ||
- TRANS | - TRANS | ||
- SPEC | - SPEC | ||
+ | - JUSTICE/ | ||
* Case sensitive | * Case sensitive | ||
Line 315: | Line 410: | ||
* '' | * '' | ||
+ | === 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.1405261668.txt.gz · Last modified: 2020-11-18 18:10 (external edit)