Formal = Mittels Logik

• $\bigwedge \emptyset = \top$
• $\bigvee \emptyset = \perp$

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
  1. Tabelle Erstellen
  2. Bei 0: Veroderung (Disjunktion) erstellen ($A=0 \Rightarrow A$ / $A=1 \Rightarrow \neg A$)
  3. Verodrungen verunden (Konjunktion)

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?

• Rekursive Funktion DPLL
  • Rein
    • (Teil) Besetzung
    • (Rest) KNF
  • Raus
    • Bessere Belegung

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.

Dieses System darf keine Lösung haben.

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:

1. ersetzen/umlenken
2. 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)

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

$AG \Leftrightarrow \neg EF(\neg \phi)$

$(S, \rightarrow)$

• Zustandsmenge: $\{(False, True), (True, False), (True, True)\}$
• Transitionsrealtion: $\{\left(\left(Fals, True\right), \left(True, False\right)\right), \ldots\}$

Interpretation enthält keine Formel.

• (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))$

1. Formel umformen (nur noch $\neg, \wedge, \perp, AF, E[\cdot U \cdot ]$)
2. Teilformeln bis auf Variablen-Ebene finden
3. Teilformeln Bottom-up durchgehen, bis nichts mehr geht
   1. 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)$

1. $\neg\phi$ für Ausblenden/Ignorieren/Streichen
2. Starke Zusammenhangskomponenten markieren (Ring-Pfad durch Knoten)
3. Markiere Knoten, die in eine echte starke Zusammenhangskomponenten zeigen

Zeitkomplexität: Linear zu Transitionen

Aber state-explosion-problem: Exponentiell mit Anzahl zu modelierender Prozesse

Teile

1. MODULE
2. VAR
3. ASSIGN
4. INIT
5. TRANS
6. 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 main

– oder –

MODULE p(x, y, z)

• Keine Typ angaben

VAR
  a : boolean;
  b : {foo, bar};
  c : process otherModule(foo, bar);

• … : … ;
• boolean
• Set: {}

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 und INVAR

Bei case: Boolscher Test: Wert/Set;

INIT
  b = foo;

• … = … ;

TRANS
    b = foo & next(b) = bar
  | b = bar & next(b) = foo
  | b = bar & next(b) = bar

• Transition, wenn Formel erfüllt

INVAR
  Ziege.pos = Wolf.pos -> Bauer.pos = Ziege.pos

• Invariante

SPEC
  AG(a -> AF b = foo)

DEFINE
  foo := myVar = foo & myOtherVAr = bar;

• … := … ;