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-13 01:37] – [CTL] 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
 +  - 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> <code>
 MODULE main MODULE main
 +</code>
 +-- oder --
 +<code>
 +MODULE p(x, y, z)
 +</code>
 +  * Keine Typ angaben
  
 +=== VAR ===
 +<code>
 VAR VAR
   a : boolean;   a : boolean;
   b : {foo, bar};   b : {foo, bar};
 +  c : process otherModule(foo, bar);
 +</code>
 +  * ''... **:** ... **;**''
 +  * ''boolean''
 +  * Set: ''{}''
  
------------------------+=== ASSIGN === 
 +<code>
 ASSIGN ASSIGN
-  init(b) := foo +  init(b) := foo; 
-  next(b) := {foo, bar}+  next(b) := {foo, bar};
   next(b) := case   next(b) := case
                foo  : bar;                foo  : bar;
                TRUE : {foo, bar};                TRUE : {foo, bar};
              esac;              esac;
--- oder ---------------+  c := !b 
 +</code> 
 +  * ''... **:=** ...**;**'' 
 +  * ''init()'' 
 +  * ''next()'' 
 +  * Invarianten 
 +  * ''case ... esac'' 
 +  * Ersetzt ''INIT'', ''TRANS'' und ''INVAR'' 
 + 
 +Bei ''case'': ''Boolscher Test: Wert/Set;'' 
 + 
 +=== INIT === 
 +<code>
 INIT INIT
-  b = foo+  b = foo
 +</code> 
 +  * ''... **=** ... **;**''
  
 +=== TRANS ===
 +<code>
 TRANS TRANS
-    b = foo & next(foo) = bar +    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 SPEC
   AG(a -> AF b = foo)   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.1405208239.txt.gz · Last modified: 2020-11-18 18:10 (external edit)