Processing math: 100%

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-13 16:27] – [SMV] skrupellosuni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1
Line 219: Line 219:
 Zeitkomplexität: Linear zu Transitionen Zeitkomplexität: Linear zu Transitionen
  
-Aber //state-explosion-problem//: Exponentiell mit Anzahl zu modelierender Prozesse+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 ==== ==== SMV ====
 Teile Teile
Line 229: Line 323:
   - TRANS   - TRANS
   - SPEC   - SPEC
 +  - JUSTICE/FAIRNESS
  
   * Case sensitive   * Case sensitive
Line 315: Line 410:
  
   * ''... **:=** ... **;**''   * ''... **:=** ... **;**''
 +=== 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.1405261668.txt.gz · Last modified: 2020-11-18 18:10 (external edit)