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, \ldots$ |
|---|---|
| Junktoren | $\neg, \wedge, \vee, \Rightarrow, \Leftrightarrow$ |
| Formel | $\phi, \psi, \ldots$ |
| Konstanten | $\top, \perp$ |
Semantik
| Belegung | $\eta$ |
|---|---|
| Foo | $⟦\phi⟧\eta$ |
| Bar | $\&, \mid\mid$ |
| Tautologie | $\forall \eta:⟦\phi⟧\eta$ |
|---|---|
| Erfüllbar | $\exists \eta:⟦\phi⟧\eta$ |
| Unerfüllbar | $\forall \eta:\neg⟦\phi⟧\eta$ |
| Äquivalent | $\forall \eta:⟦\phi⟧\eta = ⟦\psi⟧\eta$ |
| Erfüllbarkeitsäuivalenz | $(\phi \text{ und } \psi \text{ sind erfüllbar}) \vee (\phi \text{ und } \psi \text{ sind unerfüllbar})$ |
Normierung
| Literal | $A$ und $\neg A$ |
|---|---|
| Minterm | Konjunktion: $\ldots \wedge \ldots \wedge \ldots \wedge \ldots$ (Die wenigsten Belegungen sind $\top$) |
| Maxterm / Klausel | Disjunktion: $\ldots \vee \ldots \vee \ldots \vee \ldots$ (Die meisten Belegungen sind $\top$) |
| KNF | $(\ldots \vee \ldots \vee \ldots \vee \ldots ) \wedge ( \ldots \vee \ldots \vee \ldots \vee \ldots )$ |
| DNF | $(\ldots \wedge \ldots \wedge \ldots \wedge \ldots) \vee (\ldots \wedge \ldots \wedge \ldots \wedge \ldots)$ |
- $\bigwedge \emptyset = \top$
- $\bigvee \emptyset = \perp$
| $\phi$ … 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 \Leftrightarrow \phi$ als KNF
- Tabelle Erstellen
- Bei 0: Veroderung (Disjunktion) erstellen ($A=0 \Rightarrow A$ / $A=1 \Rightarrow \neg A$)
- Verodrungen verunden (Konjunktion)
| $$KNF(A) = (A, \top)$$ |
| $$\begin{array}{ll}KNF(\neg\phi) =&\text{let } (B, \Gamma) = KNF(\phi) \text{ in} \\ & (C, \Gamma \wedge (C \vee B) \wedge (\neg C \vee \neg B))\end{array}$$ |
| $$\begin{array}{ll}KNF(\phi_1\vee\phi_2) =&\text{let } (B_1, \Gamma_1) = KNF(\phi_1) \text{ in} \\ &\text{let } (B_2, \Gamma_2) = KNF(\phi_2) \text{ in} \\ & (C, \Gamma_1 \wedge \Gamma_2 \wedge (\neg C \vee B_1 \vee B_2) \wedge (C \vee \neg B_1) \wedge (C \vee \neg B_2))\end{array}$$ |
SAT-Solver
SAT
- “ist $\phi$ erfüllbar?”
- Entscheidungsproblem (NP-Hart)
- Nur für KNF
- Erweiterung auf nicht KNF: Tseitin Übersetzung
- Erweiterung auf Äquivalenz von $\phi$ und $\psi$: $\neg (\phi \Leftrightarrow \psi)$ 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\ldots$ das selbe liefern, dann darf $\neg \left( \left(f_1(x\ldots) \Leftrightarrow f'_1(x\ldots)\right) \wedge \left(f_2(x\ldots) \Leftrightarrow f'_2(x\ldots)\right)\right)$ keine Lösung liefern.
Nebenläufige Systeme
| Zeit | |||||
|---|---|---|---|---|---|
| 0 | 1 | … | n-1 | ||
| Zustand | $z_1$ | $x_{zt}$ | |||
| $z_2$ | |||||
| … | |||||
| $\bigwedge_t \bigwedge_{z \in Z} \bigwedge_{z' \ne z}\neg(x_{zt} \wedge x_{z't})$ | Zu jeder Zeit ist nur ein zustand gesetzt |
| $\bigvee_{z \in I} x_{z0}$ | Einer der Startzustände |
| $\bigwedge^{n-2}_{t=0} \bigvee_{z \rightarrow z'} x_{zt} \wedge x_{z'(t+1)}$ | Zu jeder Zeit führt ein Zustand in einen Folgezustand |
| $\bigvee^{n-1}_{t=0} \bigvee_{z \in V} x_{zt}$ | 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 \wedge f[x := \top]) \vee (\neg x \wedge f[x := \perp])$
Negation: True und False vertauschen
Variable setzen:
- ersetzen/umlenken
- reduzieren
Zweistellige Operationen: Rekursiv $(x \wedge (f[x := \top] \oplus g[x := \top])) \vee (\neg x (\wedge f[X := \perp] \oplus g[x := \perp]))$ (Gehe die Variablen der reihe nach durch. Ersetze die Nachfolger durch $\oplus$ aus den True-Zweigen und durch $\oplus$ aus den False-Zweigen.)
Alle möglichkeiten einer Variablen probieren: $\exists x: f := f[x := \top] \vee f[x :=\perp]$
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\bigwedge_p q_{p,sleep})$
- Fairness: “Gute Eigenschaft” gilt für alle fairen Abläufe
CTL
| AG | Auf allen Pfaden gilt immer … |
|---|---|
| EF | Auf einem Pfad gilt irgendwann (für immer???) … |
$AG \Leftrightarrow \neg EF(\neg \phi)$