This is an old revision of the document!
−Table of Contents
Formale Spezifikation und Verifikation
Formal = Mittels Logik
Propositionallogik
Syntax
Propositionale Variablen | A,B,C,… |
---|---|
Junktoren | ¬,∧,∨,⇒,⇔ |
Formel | ϕ,ψ,… |
Konstanten | ⊤,⊥ |
Semantik
Belegung | η |
---|---|
Foo | ⟦ϕ⟧η |
Bar | &,∣∣ |
Tautologie | ∀η:⟦ϕ⟧η |
---|---|
Erfüllbar | ∃η:⟦ϕ⟧η |
Unerfüllbar | ∀η:¬⟦ϕ⟧η |
Äquivalent | ∀η:⟦ϕ⟧η=⟦ψ⟧η |
Erfüllbarkeitsäuivalenz | (ϕ und ψ sind erfüllbar)∨(ϕ und ψ sind unerfüllbar) |
Normierung
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 |
Tseitin Übersetzung
Nur erfüllungsäquivalent
- Rekursive Funktion KNF
- Rein
- (Nicht-Normalisierte) Formel
- Raus
- Neuster (frischer) Variablenname
- KNF
- C ist frische Variable
- Regel: C⇔ϕ als KNF
- Tabelle Erstellen
- Bei 0: Veroderung (Disjunktion) erstellen (A=0⇒A / A=1⇒¬A)
- Verodrungen verunden (Konjunktion)
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-Solver
SAT
- “ist ϕ erfüllbar?”
- Entscheidungsproblem (NP-Hart)
- Nur für KNF
- Erweiterung auf nicht KNF: Tseitin Übersetzung
- Erweiterung auf Äquivalenz von ϕ und ψ: ¬(ϕ⇔ψ) unerfüllbar?
DPLL-Algorithmus
- Rekursive Funktion DPLL
- Rein
- (Teil) Besetzung
- (Rest) KNF
- Raus
- Bessere Belegung
Hier gibt es mehr. Aber das halte ich für Klausurirrelevant
Gleichheit von Schaltkreisen
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.
Nebenläufige Systeme
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.
BDD
nichtreduzierter BDDs
- Gerichtet
- Azyklisch
- Knoten auf Pfad mit fixer Ordnung (es dürfen welche fehlen)
reduzierte BDDs (zusätzlich)
- Keine Kanten mit identischen Start und Ziel (gleich ist OK)
- Keine Redundanz (isomarphen Teilgraphen)
- Nur True und False als Blätter (jeweils max. 1x)
nichtreduziert → reduziert
- Knoten mit identischen Nachfolgern entfernen
- Knoten: Name gleich & Nachfolger gleich ⇒ verschmelzen
- True/False verschmelzen.
BDDs sind eindeutig: Gleiche Funktion ⇒ isomorphe BDDs
Shannon-Zerlegung: f=(x∧f[x:=⊤])∨(¬x∧f[x:=⊥])
Negation: True und False vertauschen
Variable setzen:
- ersetzen/umlenken
- reduzieren
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
- Umordnen (extremfall: explonential)
- Teilographen wiederverwenden (Hash-Funktion zum finden)
Es fehlen nebenläufige Systeme!!!
Model checking
Arten
- Bounded (Beschränkt durch die Symulationszeit)
- SAT Solver
- Symbolic
- BDDs
Dinge die Interessieren
- Safty: Keine verbotenen Zustände erreichbar
- Liveness: Reset-Zustand immer erreichbar? Kein verklemmen AG(EF⋀pqp,sleep)
- Fairness: “Gute Eigenschaft” gilt für alle fairen Abläufe
CTL
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 |
Transitinssystem
(S,→)
- Zustandsmenge: {(False,True),(True,False),(True,True)}
- Transitionsrealtion: {((Fals,True),(True,False)),…}
Interpretationen
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.
Äquivalenz
- (AE)(GF) vertauschen und 2xnegieren
- AG(ϕ)⟺¬EF(¬ϕ)
- AF(ϕ)⟺¬EG(¬ϕ)
- EF(ϕ)⟺¬AG(¬ϕ)
- EG(ϕ)⟺¬AF(¬ϕ)
- AG(ϕ∧ψ)⟺AG(ϕ)∧AG(ψ)
- AF(ϕ)⟺A[⊤Uϕ]
- EF(ϕ)⟺E[⊤Uϕ]
- A\[ϕUψ\]⟺¬(E[¬ϕU(¬ϕ∧¬ψ)]∨EG(¬ϕ))
Labeling Algorithmus
- Formel umformen (nur noch ¬,∧,⊥,AF,E[⋅U⋅])
- Teilformeln bis auf Variablen-Ebene finden
- Teilformeln Bottom-up durchgehen, bis nichts mehr geht
- Graph mit geltenden Teilformeln markieren, bis nichts mehr geht (dabei auf bereits markiertes berufen)
Markiere mit ..
- AF(ϕ), wo ..
- ϕ
- Alle Nachfolger sind AF(ϕ)
- E[ϕUψ], wo ..
- ψ
- ϕ und Folgezustand mit E[ϕUψ]
Effizienter: EG(ϕ) anstatt AF(ϕ)
- ¬ϕ für Ausblenden/Ignorieren/Streichen
- Starke Zusammenhangskomponenten markieren (Ring-Pfad durch Knoten)
- Markiere Knoten, die in eine echte starke Zusammenhangskomponenten zeigen
Zeitkomplexität: Linear zu Transitionen
Aber state-explosion-problem: Exponentiell mit Anzahl zu modelierender Prozesse
SMV
Teile
- MODULE
- VAR
- ASSIGN
- INIT
- TRANS
- SPEC
- 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
MODULE main
– oder –
MODULE p(x, y, z)
- Keine Typ angaben
VAR
VAR a : boolean; b : {foo, bar}; c : process otherModule(foo, bar);
… : … ;
boolean
- Set:
{}
ASSIGN
ASSIGN init(b) := foo; next(b) := {foo, bar}; next(b) := case foo : bar; TRUE : {foo, bar}; esac; c := !b
… := …;
init()
next()
- Invarianten
case … esac
- Ersetzt
INIT
,TRANS
undINVAR
Bei case
: Boolscher Test: Wert/Set;
INIT
INIT b = foo;
… = … ;
TRANS
TRANS b = foo & next(b) = bar | b = bar & next(b) = foo | b = bar & next(b) = bar
- Transition, wenn Formel erfüllt
INVAR
INVAR Ziege.pos = Wolf.pos -> Bauer.pos = Ziege.pos
- Invariante
SPEC
SPEC AG(a -> AF b = foo)
DEFINE
DEFINE foo := myVar = foo & myOtherVAr = bar;
… := … ;