====== 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: Ver//oder//ung (Disjunktion) erstellen ($A=0 \Rightarrow A$ / $A=1 \Rightarrow \neg A$)
    - Verodrungen ver//und//en (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


<WRAP center round important 60%>
Hier gibt es mehr. Aber das halte ich für Klausurirrelevant
</WRAP>

==== 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)

<WRAP center round important 60%>
Es fehlen nebenläufige Systeme!!!
</WRAP>

===== 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 ====

^ Propositionale Variablen | $p, q, \ldots$ | Jedes Aussgenlogische Formel ist CTL! |
^ Junktoren | $\neg, \wedge, \vee, \Rightarrow, \Leftrightarrow$ | ::: |
^ Formel | $\phi, \psi, \ldots$ | ::: |
^ Konstanten | $\top, \perp$ | ::: |
^ Foo | $AX, EX, A[\phi U \psi], E[\phi U \psi], AG \phi, AF \phi, EG \phi, EF \phi$ | |


$AG \Leftrightarrow \neg EF(\neg \phi)$
<WRAP second column>
^A|Auf allen Pfaden gilt ...|
^E|Auf (mindestens) einem Pfad gilt ...|
</WRAP>
<WRAP second column>
...in...
</WRAP>
<WRAP second column>
^X|Ne**x**t|... (mindestens) einem unmittelbar folgenden Zustand|
^F|**F**inal|... (mindestens) einem folgenden/selben Zustand|
^G|**G**lobaly|... allen folgenden/selben Zuständen|
^U|**U**ntil|... allen folgenden/selben Zuständen $\phi$, bis $\psi$ gilt. \\ $\psi$ kann bereits im selben gelten|
</WRAP>

=== Transitinssystem ===
$(S, \rightarrow)$

  * Zustands//menge//: $\{(False, True), (True, False), (True, True)\}$
  * Transitionsrealtion: $\{\left(\left(Fals, True\right), \left(True, False\right)\right), \ldots\}$

===Interpretationen===
^ $Tr(\mathcal{I})$ | $(S, \rightarrow)$ | Transitionsystem | Durch $\mathcal{I}$ festgelegt |
^ $\mathcal{I}(p)$  | $\subseteq S$ | Zustände in denen $p$ gilt | ::: |
^ $s \models \mathcal{I} p$ | $\{True, False\}$ | Aussage: $p$ ist in Zustand $s$ gesetzt | ::: |
^ $\mathcal{I}(\phi)$  | $\subseteq S$ | Zustände in denen $\phi$ gilt | Ableitbar |
^ $s \models \mathcal{I} \phi$ | $\{True, False\}$ | Aussage: $\phi$ ist in Zustand $s$ gesetzt | ::: |

Interpretation enthält keine Formel.

===Äquivalenz ===
  * (AE)(GF) vertauschen und 2xnegieren
    * $AG(\phi) \Longleftrightarrow \neg EF(\neg \phi)$
    * $AF(\phi) \Longleftrightarrow \neg EG(\neg \phi)$
    * $EF(\phi) \Longleftrightarrow \neg AG(\neg \phi)$
    * $EG(\phi) \Longleftrightarrow \neg AF(\neg \phi)$
  * $AG(\phi \wedge \psi) \Longleftrightarrow AG(\phi) \wedge AG(\psi)$
  * $AF(\phi) \Longleftrightarrow A[\top U \phi]$
  * $EF(\phi) \Longleftrightarrow E[\top U \phi]$
  * $A\[\phi U \psi\] \Longleftrightarrow \neg (E[\neg \phi U (\neg \phi \wedge \neg \psi)] \vee EG(\neg \phi))$

=== Labeling Algorithmus ===
  - Formel umformen (nur noch $\neg, \wedge, \perp, AF, E[\cdot U \cdot ]$)
  - 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(\phi)$, wo ..
    * $\phi$
    * Alle Nachfolger sind $AF(\phi)$
  * $E[\phi U \psi]$, wo ..
    * $\psi$
    * $\phi$ und Folgezustand mit $E[\phi U \psi]$

Effizienter: $EG(\phi)$ anstatt $AF(\phi)$
  - $\neg\phi$ 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 \\ => BDDs verhindern das (es kann optimiert werden)

=== Fairnes ===
Alle interessierenden Zustände können immer unendlich offt erreicht werden.

  * D.h. für ''E?'', es Existiert ein fairer Pfad in dem ...
  * D.h. für ''A?'', in allen fairen Pfaden gild ...

Abwandlung des Labeling Algorithmuses:
  * Starke Zusammenhangskomponente ist fair, wenn ein Zustand Fairnesbedingung erfüllt
  * Zustand ist fair, wenn ein (längerer) Pfad zu fairen starken Zusamenhangskomponente existiert

=== Encoding of CTL in BDD ===
BDD ist ein Bitvektor und daher kann ich ein Transitionsystem eincodieren, sowie ein $\phi$.

http://nicta.com.au/__data/assets/pdf_file/0018/14814/lecture4-mc2.pdf

<WRAP center round important 60%>
ToDo
</WRAP>

==== LTL ====
^ Propositionale Variablen | $p, q, \ldots$ | **eingeschränktes** CTL! |
^ Junktoren | $\neg, \wedge$ | ::: |
^ Formel | $\phi, \psi, \ldots$ | ::: |
^ Konstanten | $\top$ | ::: |
^ Foo | $X \phi, F \phi, G \phi, \phi U \psi$ | |

  * Fairness direkt angebbar: ''**(GF** p1.state=running**) =>** ...''
  * CTL ist ausdrucksstärker
  * Für **alle** Pfade muss ... gelten

==== Büchi Automat ====
$(\Sigma, T, I, E, \delta)$

| $\Sigma$ | Menge | Alphabet |
| $Z$ | Menge | Zustände |
| $I$ | Menge | Anfangszustände |
| $E$ | Menge | Endzustände |
| $\delta$ | Relation | Zustandsübergänge |

  * Nichtdeterministisch
  * Unendliche Wörter
  * Akzeptiert: Wenn mindestens ein Lauf //existiert//, der immer zu einem Endzustand kommen (unendlich offt)

$L = (b^{*}a)^\omega$ (wenn ''a'' immer wieder vorkommen muss)

| $\omega$ | FG | Unendlich offt vorkommen |
| $*$      | GF | Endlich offt vorkommen   |

===== Typanalyse =====
==== While Programm ====
  * ''**while [**...**] do **...''
  * ''**if [**...**] then **...** else **...''
  * ''**true**''
  * ''**false**''
  * ''**not **...''
  * ''... **:= **...''
  * Aritmetische Ausdrücke
  * Boolsche Ausdrücke

==== Datenflussgleichung ====
"Erreichbare Definitionen" (Reachable Definitions)

  * $RD_{{\color{ForestGreen}entry}}(\ell) = \bigcup_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}RD_{exit}({\color{red}\ell'})$
  * $RD_{exit}(\ell) = (RD_{{\color{ForestGreen}entry}}(\ell) \setminus \text{"Entwertete Zuweisungen"}) \cup \text{ "Neue Zuweisungen"}$
  * Zu beginn werden //alle// Variablen mit "$(X, \ell)$" initialisiert.



"Verfügbare Ausdrücke" (Available Expressions)
  * $AE_{{\color{ForestGreen}entry}}(\ell) = {\color{blue}\bigcap}_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}AE_{exit}({\color{red}\ell'})$
  * $AE_{exit}(\ell) = (AE_{{\color{ForestGreen}entry}}(\ell) \setminus kill_{AE}(B^\ell)) \cup gen_{AE}(B^\ell)$
  * $kill_{AE}([x:=a]^\ell) = \{\text{Formeln, die }x\text{ enthalten}\}$
  * $gen_{AE}([x := a]) = \{\text{Teilausdrücke von }a\text{ ohne }x\}$
  * $gen_{AE}([bool\ exp]) = \{\text{Teilausdrücke von }bool\ exp\}$
  * Zu beginn werden //alle// Variablen mit "$\emptyset$" initialisiert.
  * //Nur// Arithmetische Ausdrücke


"Lebendige Variablen" (Live Variables)
  * $LV_{exit}(\ell) = \bigcup_{{\color{red}\ell'}:\ell\rightarrow{\color{red}\ell'}}LV_{{\color{ForestGreen}entry}}({\color{red}\ell'})$
  * $LV_{{\color{ForestGreen}entry}}(\ell) = (LV_{exit}(\ell) \setminus kill_{LV}(B^\ell)) \cup gen_{LV}(B^\ell)$
  * $kill_{LV}([x:=a]^\ell) = \{x\}$
  * $gen_{LV}([x := a]) = \{\text{Variablen in }a\}$
  * $gen_{LV}([bool\ exp]) = \{\text{Variablen in }bool\ exp\}$
  * Zu beginn werden //alle// Variablen mit "$\emptyset$" initialisiert.

^ $\ell$ ^ $RD_{entry}(\ell)$ ^ $RD_{exit}(\ell)$ ^
| 1 | (x, ?), (y, ?) | ... |
| 2 | ... | ... |
| 3 | ... | ... |

So lange ausfüllen, bis nichts mehr geht.

Das geht, weil //Fixpunkte// und //Knaster-Tarski-Theorem//
==== SMV ====
Teile
  - MODULE
  - VAR
  - ASSIGN
  - INIT
  - TRANS
  - SPEC
  - JUSTICE/FAIRNESS

  * 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 ===
<code>
MODULE main
</code>
-- oder --
<code>
MODULE p(x, y, z)
</code>
  * Keine Typ angaben

=== VAR ===
<code>
VAR
  a : boolean;
  b : {foo, bar};
  c : process otherModule(foo, bar);
</code>
  * ''... **:** ... **;**''
  * ''boolean''
  * Set: ''{}''

=== ASSIGN ===
<code>
ASSIGN
  init(b) := foo;
  next(b) := {foo, bar};
  next(b) := case
               foo  : bar;
               TRUE : {foo, bar};
             esac;
  c := !b
</code>
  * ''... **:=** ...**;**''
  * ''init()''
  * ''next()''
  * Invarianten
  * ''case ... esac''
  * Ersetzt ''INIT'', ''TRANS'' und ''INVAR''

Bei ''case'': ''Boolscher Test: Wert/Set;''

=== INIT ===
<code>
INIT
  b = foo;
</code>
  * ''... **=** ... **;**''

=== TRANS ===
<code>
TRANS
    b = foo & next(b) = bar
  | b = bar & next(b) = foo
  | b = bar & next(b) = bar
</code>

  * Transition, wenn Formel erfüllt

=== INVAR ===
<code>
INVAR
  Ziege.pos = Wolf.pos -> Bauer.pos = Ziege.pos
</code>
  * Invariante

=== SPEC ===
<code>
SPEC
  AG(a -> AF b = foo)
</code>

=== DEFINE ===
<code>
DEFINE
  foo := myVar = foo & myOtherVAr = bar;
</code>

  * ''... **:=** ... **;**''
=== JUSTICE/FAIRNESS ===
<code>
JUSTICE/FAIRNESS
  p1.status = running
</code>

===== Beweise =====
==== Vollständiger Verband ====
Verband $(L, \sqsubseteq)$
  * **reflexiv** \\ $\forall_{x \in L} : x \sqsubseteq x$
  * **transitiv** \\ $\forall_{x, y, z \in L} : x \sqsubseteq y \wedge y \sqsubseteq z \Rightarrow x \sqsubseteq z$
  * **antisymetrisch** \\ $\forall_{x, y \in L} : x \sqsubseteq y \wedge y \sqsubseteq x \Rightarrow x = y$
  * **Jede Teilmenge hat ein Supremum** \\ Jedes $U \subseteq L$ hat ein $\bigsqcup U$

==== Supremum ====
$s = \bigsqcup U$

  * **Ist obere Schranke** \\ $\forall_{x \in U} : x \sqsubseteq s$
  * **Ist //kleinste// obere Schranke** \\ $s' \text{ ist obere Schranke } \Rightarrow s \sqsubseteq s'$

==== Monotonie ====
  * $x \sqsubseteq y \Rightarrow F(x) \sqsubseteq F(y)$
 
==== Fixpunkt ====
  * $\exists x: F(x) = x$

Dazu muss $F(x)$ monoton sein.
===== Probleme =====
==== Semaphor ====
==== Alternating Bit Protocol ====
  * Zwei Kommunikationspartner
  * Bidirektionaler Kanal
  * Nachricht: OK/Defekt
  * So lange wiederholen bis es klapt

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 | ::: |