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-12 15:54] – [BDD] skrupellosuni: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 p,q, | Jedes Aussgenlogische Formel ist CTL! 
 +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>
 +<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.1405173272.txt.gz · Last modified: 2020-11-18 18:10 (external edit)