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-15 15:30] – [CTL] skrupellos | uni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1 | ||
---|---|---|---|
Line 249: | Line 249: | ||
* Fairness direkt angebbar: '' | * Fairness direkt angebbar: '' | ||
* CTL ist ausdrucksstärker | * CTL ist ausdrucksstärker | ||
+ | * Für **alle** Pfade muss ... gelten | ||
==== Büchi Automat ==== | ==== Büchi Automat ==== | ||
Line 280: | Line 281: | ||
==== Datenflussgleichung ==== | ==== Datenflussgleichung ==== | ||
- | "Reichweite von Zuweisungen" | + | "Erreichbare Definitionen" |
- | * $RD_{exit}(\ell) = (RD_{exit}(\ell) \setminus \text{" | + | * $RD_{{\color{ForestGreen}entry}}(\ell) = \bigcup_{{\color{red}\ell' |
- | * $RD_{entry}(\ell) = \bigcup_{\ell': | + | * $RD_{exit}(\ell) = (RD_{{\color{ForestGreen}entry}}(\ell) \setminus \text{" |
- | * Zu beginn werden //alle// Variablen mit "(X, ?)" initialisiert. | + | * Zu beginn werden //alle// Variablen mit "$(X, \ell)$" |
+ | |||
+ | |||
+ | |||
+ | " | ||
+ | * $AE_{{\color{ForestGreen}entry}}(\ell) = {\color{blue}\bigcap}_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}AE_{exit}({\color{red}\ell'})$ | ||
+ | * AEexit(ℓ)=(AEentry(ℓ)∖killAE(Bℓ))∪genAE(Bℓ) | ||
+ | * killAE([x:=a]ℓ)={Formeln, die x enthalten} | ||
+ | * genAE([x:=a])={Teilausdrücke von a ohne x} | ||
+ | * $gen_{AE}([bool\ exp]) = \{\text{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(ℓ) ^ | ^ ℓ ^ RDentry(ℓ) ^ RDexit(ℓ) ^ | ||
Line 291: | Line 312: | ||
| 3 | ... | ... | | | 3 | ... | ... | | ||
+ | So lange ausfüllen, bis nichts mehr geht. | ||
+ | |||
+ | Das geht, weil // | ||
==== SMV ==== | ==== SMV ==== | ||
Teile | Teile | ||
Line 392: | Line 416: | ||
</ | </ | ||
+ | ===== 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 ===== | ===== Probleme ===== | ||
==== Semaphor ==== | ==== Semaphor ==== |
uni/6/fsv/start.1405431012.txt.gz · Last modified: 2020-11-18 18:10 (external edit)