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?