Formal = Mittels Logik
Propositionale Variablen | A,B,C,… |
---|---|
Junktoren | ¬,∧,∨,⇒,⇔ |
Formel | ϕ,ψ,… |
Konstanten | ⊤,⊥ |
Belegung | η |
---|---|
Foo | ⟦ϕ⟧η |
Bar | &,∣∣ |
Tautologie | ∀η:⟦ϕ⟧η |
---|---|
Erfüllbar | ∃η:⟦ϕ⟧η |
Unerfüllbar | ∀η:¬⟦ϕ⟧η |
Äquivalent | ∀η:⟦ϕ⟧η=⟦ψ⟧η |
Erfüllbarkeitsäuivalenz | (ϕ und ψ sind erfüllbar)∨(ϕ und ψ sind unerfüllbar) |
Literal | A und ¬A |
---|---|
Minterm | Konjunktion: …∧…∧…∧… (Die wenigsten Belegungen sind ⊤) |
Maxterm / Klausel | Disjunktion: …∨…∨…∨… (Die meisten Belegungen sind ⊤) |
KNF | (…∨…∨…∨…)∧(…∨…∨…∨…) |
DNF | (…∧…∧…∧…)∨(…∧…∧…∧…) |
ϕ … KNF | Größe | Zeit |
---|---|---|
Äquivalent | exponentiell | ? |
Erfüllungsäuivalent | linear | polynomiell |
Nur erfüllungsäquivalent
KNF(A)=(A,⊤) |
KNF(¬ϕ)=let (B,Γ)=KNF(ϕ) in(C,Γ∧(C∨B)∧(¬C∨¬B)) |
KNF(ϕ1∨ϕ2)=let (B1,Γ1)=KNF(ϕ1) inlet (B2,Γ2)=KNF(ϕ2) in(C,Γ1∧Γ2∧(¬C∨B1∨B2)∧(C∨¬B1)∧(C∨¬B2)) |
SAT
Hier gibt es mehr. Aber das halte ich für Klausurirrelevant
Wenn gezeigt werden soll, das die Schaltungen f und f′ bezüglich ihrer Eingänge x… das selbe liefern, dann darf ¬((f1(x…)⇔f′1(x…))∧(f2(x…)⇔f′2(x…))) keine Lösung liefern.
Zeit | |||||
---|---|---|---|---|---|
0 | 1 | … | n-1 | ||
Zustand | z1 | xzt | |||
z2 | |||||
… |
⋀t⋀z∈Z⋀z′≠z¬(xzt∧xz′t) | Zu jeder Zeit ist nur ein zustand gesetzt |
⋁z∈Ixz0 | Einer der Startzustände |
⋀n−2t=0⋁z→z′xzt∧xz′(t+1) | Zu jeder Zeit führt ein Zustand in einen Folgezustand |
⋁n−1t=0⋁z∈Vxzt | Zu einer Zeit ist ein verbotener Zustand erreicht |
Dieses System darf keine Lösung haben.
nichtreduzierter BDDs
reduzierte BDDs (zusätzlich)
nichtreduziert → reduziert
BDDs sind eindeutig: Gleiche Funktion ⇒ isomorphe BDDs
Shannon-Zerlegung: f=(x∧f[x:=⊤])∨(¬x∧f[x:=⊥])
Negation: True und False vertauschen
Variable setzen:
Zweistellige Operationen: Rekursiv (x∧(f[x:=⊤]⊕g[x:=⊤]))∨(¬x(∧f[X:=⊥]⊕g[x:=⊥])) (Gehe die Variablen der reihe nach durch. Ersetze die Nachfolger durch ⊕ aus den True-Zweigen und durch ⊕ aus den False-Zweigen.)
Alle möglichkeiten einer Variablen probieren: ∃x:f:=f[x:=⊤]∨f[x:=⊥]
Optiomierungen
Es fehlen nebenläufige Systeme!!!
Arten
Dinge die Interessieren
Propositionale Variablen | p,q,… | Jedes Aussgenlogische Formel ist CTL! |
---|---|---|
Junktoren | ¬,∧,∨,⇒,⇔ | |
Formel | ϕ,ψ,… | |
Konstanten | ⊤,⊥ | |
Foo | AX,EX,A[ϕUψ],E[ϕUψ],AGϕ,AFϕ,EGϕ,EFϕ |
AG⇔¬EF(¬ϕ)
A | Auf allen Pfaden gilt … |
---|---|
E | Auf (mindestens) einem Pfad gilt … |
…in…
X | Next | … (mindestens) einem unmittelbar folgenden Zustand |
---|---|---|
F | Final | … (mindestens) einem folgenden/selben Zustand |
G | Globaly | … allen folgenden/selben Zuständen |
U | Until | … allen folgenden/selben Zuständen ϕ, bis ψ gilt. ψ kann bereits im selben gelten |
(S,→)
Tr(I) | (S,→) | Transitionsystem | Durch I festgelegt |
---|---|---|---|
I(p) | ⊆S | Zustände in denen p gilt | |
s⊨Ip | {True,False} | Aussage: p ist in Zustand s gesetzt | |
I(ϕ) | ⊆S | Zustände in denen ϕ gilt | Ableitbar |
s⊨Iϕ | {True,False} | Aussage: ϕ ist in Zustand s gesetzt |
Interpretation enthält keine Formel.
Markiere mit ..
Effizienter: EG(ϕ) anstatt AF(ϕ)
Zeitkomplexität: Linear zu Transitionen
Aber state-explosion-problem: Exponentiell mit Anzahl zu modelierender Prozesse
⇒ BDDs verhindern das (es kann optimiert werden)
Alle interessierenden Zustände können immer unendlich offt erreicht werden.
E?
, es Existiert ein fairer Pfad in dem …
A?
, in allen fairen Pfaden gild …
Abwandlung des Labeling Algorithmuses:
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
ToDo
Propositionale Variablen | p,q,… | eingeschränktes CTL! |
---|---|---|
Junktoren | ¬,∧ | |
Formel | ϕ,ψ,… | |
Konstanten | ⊤ | |
Foo | Xϕ,Fϕ,Gϕ,ϕUψ |
(GF p1.state=running) ⇒ …
(Σ,T,I,E,δ)
Σ | Menge | Alphabet |
Z | Menge | Zustände |
I | Menge | Anfangszustände |
E | Menge | Endzustände |
δ | Relation | Zustandsübergänge |
L=(b∗a)ω (wenn a
immer wieder vorkommen muss)
ω | FG | Unendlich offt vorkommen |
∗ | GF | Endlich offt vorkommen |
while […] do …
if […] then … else …
true
false
not …
… := …
“Erreichbare Definitionen” (Reachable Definitions)
“Verfügbare Ausdrücke” (Available Expressions)
“Lebendige Variablen” (Live Variables)
ℓ | RDentry(ℓ) | RDexit(ℓ) |
---|---|---|
1 | (x, ?), (y, ?) | … |
2 | … | … |
3 | … | … |
So lange ausfüllen, bis nichts mehr geht.
Das geht, weil Fixpunkte und Knaster-Tarski-Theorem
Teile
&
bzw. |
->
für ⇒
MODULE main
– oder –
MODULE p(x, y, z)
VAR a : boolean; b : {foo, bar}; c : process otherModule(foo, bar);
… : … ;
boolean
{}
ASSIGN init(b) := foo; next(b) := {foo, bar}; next(b) := case foo : bar; TRUE : {foo, bar}; esac; c := !b
… := …;
init()
next()
case … esac
INIT
, TRANS
und INVAR
Bei case
: Boolscher Test: Wert/Set;
INIT b = foo;
… = … ;
TRANS b = foo & next(b) = bar | b = bar & next(b) = foo | b = bar & next(b) = bar
INVAR Ziege.pos = Wolf.pos -> Bauer.pos = Ziege.pos
SPEC AG(a -> AF b = foo)
DEFINE foo := myVar = foo & myOtherVAr = bar;
… := … ;
JUSTICE/FAIRNESS p1.status = running
Verband (L,⊑)
s=⨆U
Dazu muss F(x) monoton sein.
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 |