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-15 23:36] – [Datenflussgleichung] skrupellosuni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1
Line 249: Line 249:
   * Fairness direkt angebbar: ''**(GF** p1.state=running**) =>** ...''   * Fairness direkt angebbar: ''**(GF** p1.state=running**) =>** ...''
   * CTL ist ausdrucksstärker   * CTL ist ausdrucksstärker
 +  * Für **alle** Pfade muss ... gelten
  
 ==== Büchi Automat ==== ==== Büchi Automat ====
Line 283: Line 284:
  
   * RDentry()=:RDexit()   * RDentry()=:RDexit()
-  * $RD_{exit}(\ell) = (RD_{exit}(\ell) \setminus \text{"Entwertete Zuweisungen"}) \cup \text{ "Neue Zuweisungen"}$+  * $RD_{exit}(\ell) = (RD_{{\color{ForestGreen}entry}}(\ell) \setminus \text{"Entwertete Zuweisungen"}) \cup \text{ "Neue Zuweisungen"}$
   * Zu beginn werden //alle// Variablen mit "(X,)" initialisiert.   * Zu beginn werden //alle// Variablen mit "(X,)" initialisiert.
  
Line 289: Line 290:
  
 "Verfügbare Ausdrücke" (Available Expressions) "Verfügbare Ausdrücke" (Available Expressions)
-  * $AE_{{\color{ForestGreen}entry}}(\ell) = \bigcap_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}AE_{exit}({\color{red}\ell'})$ +  * $AE_{{\color{ForestGreen}entry}}(\ell) = {\color{blue}\bigcap}_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}AE_{exit}({\color{red}\ell'})$ 
-  * $AE_{exit}(\ell) = (AE_{exit}(\ell) \setminus kill_{AE}(B^\ell)) \cup gen_{AE}(B^\ell)$+  * $AE_{exit}(\ell) = (AE_{{\color{ForestGreen}entry}}(\ell) \setminus kill_{AE}(B^\ell)) \cup gen_{AE}(B^\ell)$
   * killAE([x:=a])={Formeln, die x enthalten}   * killAE([x:=a])={Formeln, die x enthalten}
-  * $gen_{AE}([x := a]) = \{\text{Teilausdrücke von }a\text{ und }x \not\in a\}$ +  * $gen_{AE}([x := a]) = \{\text{Teilausdrücke von }a\text{ ohne }x\}$ 
-  * genAE([boolexp])={Teilausdrücke von boolexp}+  * $gen_{AE}([boolexp]) = \{\text{Teilausdrücke von }boolexp\}$
   * Zu beginn werden //alle// Variablen mit "" initialisiert.   * Zu beginn werden //alle// Variablen mit "" initialisiert.
 +  * //Nur// Arithmetische Ausdrücke
 +
  
 "Lebendige Variablen" (Live Variables) "Lebendige Variablen" (Live Variables)
Line 300: Line 303:
   * LVentry()=(LVexit()killLV(B))genLV(B)   * LVentry()=(LVexit()killLV(B))genLV(B)
   * killLV([x:=a])={x}   * killLV([x:=a])={x}
-  * $gen_{LV}([x := a]) = \{\text{Teilausdrücke von }a\}$ +  * $gen_{LV}([x := a]) = \{\text{Variablen in }a\}$ 
-  * $gen_{LV}([bool exp]) = \{\text{Teilausdrücke von }bool exp\}$+  * $gen_{LV}([boolexp]) = \{\text{Variablen in }boolexp\}$
   * Zu beginn werden //alle// Variablen mit "" initialisiert.   * Zu beginn werden //alle// Variablen mit "" initialisiert.
  
Line 413: Line 416:
 </code> </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 ===== ===== Probleme =====
 ==== Semaphor ==== ==== Semaphor ====
uni/6/fsv/start.1405460170.txt.gz · Last modified: 2020-11-18 18:10 (external edit)