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

Rekursive Funktion KNF
- Rein
  - (Nicht-Normalisierte) Formel
- Raus
  - Neuster (frischer) Variablenname
  - KNF
C ist frische Variable
Regel: $C \Leftrightarrow \phi$ als KNF
1. Tabelle Erstellen
2. Bei 0: Veroderung (Disjunktion) erstellen ( $A=0 \Rightarrow A$ / $A=1 \Rightarrow \neg A$ )
3. 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 := ])$