Korrektheit Reaktiver Systeme

Transitionssystem

$\mathcal{T}=\left(S,\rightarrow,r\right)$

Zustände

$S$

Transitionsrelation

$\rightarrow\subseteq S\times S$

• infix notiert: $s\rightarrow t\Leftrightarrow\left(s,t\right)\in\rightarrow$

Anfangszustand

$r\in S$a

Pfad

der Länge $n$, mit $\forall i,0\le i\le n:s_{i}\rightarrow s_{i+1}$

$$w=s_{0}\ldots s_{n}$$

Ausführung

falls $\forall i,0\le i:s_{i}\rightarrow s_{i+1}$

$$p=s_{0}s_{1}\ldots$$

Wörter

$S^{*}$sind endlich, $S^{\omega}$ sind unendlich

Element

$\rho\left(i\right)$ ist das $i$-te Element von $\rho$ (ab 0 Zählen!)

Suffix

$\rho^{i}$ ist das bei $i$ beginnende suffix von $\rho$ (ab 0 Zählen!)

Kripke Struktur

$\mathcal{K}=\left(S,\rightarrow,r,AP,\nu\right)$

Transitionssystem

das zugrunde liegt $\left(S,\rightarrow,r\right)$

Grundaussagen

Menge $AP$

Interpretationen

der Grundaussagen $\nu:AP\rightarrow2^{S}$

• Die Zustände haben als eine Menge von Flags

Bild

$\nu^{-1}\left(\rho\right)\in\left(2^{AP}\right)^{\omega}$ kann jeder Ausführung $\rho$ zugeordnet werden: $\nu^{-1}\left(\rho\right)\left(i\right)=\left\{ a\in AP\vert\rho\left(i\right)\in\nu\left(a\right)\right\}$

erfüllt

$\mathcal{K}$ erfüllt eine LTL Formel $\phi$ (geschrieben $\mathcal{K}\models\phi$) falls für alle bei $r$ beginnenden Ausführungen $\rho$ gilt, dass $\nu^{-1}\left(\rho\right)\subseteq\left[\left[\phi\right]\right]$

• Es kann sowohl $\mathcal{K}\nvDash\phi$ als auch $\mathcal{K}\models\phi$ gelten!

LTL

Formeln

• Ist $a\in AP$ so ist $a$ eine Formel
• Sind $\phi_{1},\phi_{2}$ Formeln, so auch $\neg\phi_{1},\phi_{1}\vee\phi_{2},\textrm{X}\phi_{1},\phi_{1}\textrm{U}\phi_{2}$
• Jede Formel definiert eine Menge von Wörtern aus $\left(2^{AP}\right)^{\omega}$. Sei $\sigma\in\left(2^{AP}\right)^{\omega}$
• Semantik $\left[\left[\phi\right]\right]=\left\{ \sigma\vert\sigma\models\phi\right\}$
  

  gilt	falls
  $\sigma\models a$	$a\in\sigma\left(0\right)$
  $\sigma\models\neg\phi$	$\sigma\nvDash\phi$
  $\sigma\models\phi_{1}\vee\phi_{2}$	$\sigma\models\phi_{1}$ oder $\sigma\models\phi_{2}$
  $\sigma\models\textrm{X}\phi$	$\sigma^{1}\models\phi$
  $\sigma\models\phi_{1}\textrm{U}\phi_{2}$	$\exists i:\left(\sigma^{i}\models\phi_{2}\wedge\forall k<i:\sigma^{k}\models\phi_{1}\right)$

• $\phi_{1}\wedge\phi_{2}\equiv\neg\left(\neg\phi_{1}\vee\neg\phi_{2}\right)$
• $\textrm{true}\equiv a\vee\neg a$
• $\textrm{false}\equiv\neg\textrm{true}$
• $\textrm{F}\phi\equiv\textrm{true U}\phi$
• $\textrm{G}\phi\equiv\neg\textrm{F}\neg\phi$
• $\phi_{1}\textrm{W}\phi_{2}\equiv\left(\phi_{1}\textrm{U}\phi_{2}\right)\vee\textrm{G}\phi_{1}$
• $\phi_{1}\textrm{R}\phi_{2}\equiv\neg\left(\neg\phi_{1}\textrm{U}\neg\phi_{2}\right)$
• $\textrm{X}\left(\phi_{1}\vee\phi_{2}\right)\equiv\textrm{X}\phi_{1}\vee\textrm{X}\phi_{2}$
• $\textrm{X}\left(\phi_{1}\wedge\phi_{2}\right)\equiv\textrm{X}\phi_{1}\wedge\textrm{X}\phi_{2}$
• $\textrm{X}\neg\phi\equiv\neg\textrm{X}\phi$
• $\textrm{F}\left(\phi_{1}\vee\phi_{2}\right)\equiv\textrm{F}\phi_{1}\vee\textrm{F}\phi_{2}$
• $\textrm{G}\neg\phi\equiv\neg\textrm{F}\phi$
• $\textrm{G}\left(\phi_{1}\wedge\phi_{2}\right)\equiv\textrm{G}\phi_{1}\wedge\textrm{G}\phi_{2}$
• $\left(\phi_{1}\wedge\phi_{2}\right)\textrm{U}\psi\equiv\left(\phi_{1}\textrm{U}\psi\right)\wedge\left(\phi_{2}\textrm{U}\psi\right)$
• $\phi\textrm{U}\left(\psi_{1}\vee\psi_{2}\right)\equiv\left(\phi\textrm{U}\psi_{1}\right)\vee\left(\phi\textrm{U}\psi_{2}\right)$
• $\textrm{F}\phi\equiv\textrm{FF}\phi$
• $\textrm{G}\phi\equiv\textrm{GG}\phi$
• $\phi\textrm{U}\psi\equiv\phi\textrm{U}\left(\phi\textrm{U}\psi\right)$
• $\textrm{F}\equiv\phi\vee\textrm{XF}\phi$
• $\textrm{G}\equiv\phi\wedge\textrm{XG}\phi$
• $\phi\textrm{U}\psi\equiv\psi\vee\left(\phi\wedge\textrm{X}\left(\phi\textrm{U}\psi\right)\right)$
• $\phi\textrm{W}\psi\equiv\psi\vee\left(\phi\wedge\textrm{X}\left(\phi\textrm{W}\psi\right)\right)$

Büchi-Automat

$\mathcal{B}=\left(Q,\Sigma,\delta,q_{0},F\right)$

Zustandsmenge

(endlich) $Q$

Alphabet

(endlich) $\Sigma$

Übergangsrelation

$\delta\subseteq Q\times\Sigma\times Q$

Anfangszustand

$q_{0}\in Q$

akzeptierende

Zustände $F\subseteq Q$

akzeptiert

$\mathcal{B}$ akzeptiert $a_{0}a_{1}\ldots\in\Sigma^{\omega}$, gdw.

• $\left(q_{i},a_{i},q_{i+1}\right)\in\delta$ für alle $i\ge0$
• Es gilt $q_{i}\in F$ für unendlich viele $i$

Sprache

$\mathcal{L}\left(\mathcal{B}\right)=\left\{ \sigma\in\Sigma^{\omega}\vert\mathcal{B}\textrm{ akzeptiert }\sigma\right\}$

• von Büchi Automaten erkannte Sprachen heißen $\omega$-regulär

Generalisierter Büchi Automat

hat eine Menge $\mathcal{F}=\left\{ F_{1},\ldots,F_{n}\right\}$ von Akzeptanzmengen. Er akzeptiert, falls unenedlich viele zustände in $F_{i}$ für jedes $i$.

markiertes Produckt

$\mathcal{B}_{1}\times\mathcal{B}_{2}=\left(Q,\Sigma,\delta,q_{0},F\right)$

gegeben

$\mathcal{B}_{1}=\left(Q_{1},\Sigma,\delta_{1},q_{1},F_{1}\right)$ und $\mathcal{B}_{2}=\left(Q_{2},\Sigma,\delta_{2},q_{2},F_{2}\right)$

• $Q=Q_{1}\times Q_{2}\times\left\{ 1,2\right\}$
  

  gilt	falls
  $\in\delta$	$\in\delta_{1}$	$\in\delta_{2}$
  $\left(\left\langle s,t,1\right\rangle ,a,\left\langle s',t',1\right\rangle \right)$	$\left(s,a,s'\right)$	$\left(t,a,t'\right)$	$s\notin F_{1}$
  $\left(\left\langle s,t,1\right\rangle ,a,\left\langle s',t',2\right\rangle \right)$	$\left(s,a,s'\right)$	$\left(t,a,t'\right)$	$s\in F_{1}$
  $\left(\left\langle s,t,2\right\rangle ,a,\left\langle s',t',2\right\rangle \right)$	$\left(s,a,s'\right)$	$\left(t,a,t'\right)$	$t\notin F_{2}$
  $\left(\left\langle s,t,2\right\rangle ,a,\left\langle s',t',1\right\rangle \right)$	$\left(s,a,s'\right)$	$\left(t,a,t'\right)$	$t\in F_{2}$

• $q_{0}=\left\langle q_{1},q_{2},1\right\rangle$
• $F=F_{1}\times Q_{2}\times\left\{ 1\right\}$

LTL  $\rightarrow$generalisierter Büchi

 

gegeben

LTL-Formel $\phi$ in Normalform, d.h. Negationen sind nach Innen geschoben.

gesucht

$\mathcal{B}_{\phi}=\left(Q,\Sigma,\delta,q,F\right)$

Abschluss

$Cl\left(\phi\right)$ einer Formel $\phi$ ist die Menge aller Unterformeln von $\phi$ und ihrer Negierungen

Alphabet

$\Sigma=2^{AP}$ mit $AP$ den Atomen von $\phi$

Zustände

$Q=$ Elemente von $2^{Cl\left(\phi\right)}$, die folgende Zusatzbedingungen erfüllen

• $\forall\phi_{1}\in Cl\left(\phi\right):\neg\phi_{1}\in Q\Leftrightarrow\phi_{1}\notin Q$
• $\forall\phi_{1}\wedge\phi_{2}\in Cl\left(\phi\right):\phi_{1}\wedge\phi_{2}\in Q\Leftrightarrow\phi_{1}\in Q\wedge\phi_{2}\in Q$
• $\forall\phi_{1}\vee\phi_{2}\in Cl\left(\phi\right):\phi_{1}\vee\phi_{2}\in Q\Leftrightarrow\phi_{1}\in Q\vee\phi_{2}\in Q$

Anfangszustände,

alle die $\phi$ enthalten

Übergänge

$s{{l\atop \rightarrow}}t$, falls $l=\left\{ p\in AP\vert p\in s\right\}$, sowie

• $\forall\textrm{X}\phi_{1}\in Cl\left(\phi\right):\textrm{X}\phi_{1}\in s\Leftrightarrow\phi_{1}\in t$
• $\forall\phi_{1}\textrm{U}\phi_{2}\in Cl\left(\phi\right):\phi_{1}\textrm{U}\ph... ...phi_{2}\in s\vee\left(\phi_{1}\in s\wedge\phi_{1}\textrm{U}\phi_{2}\in t\right)$
• $\forall\phi_{1}\textrm{R}\phi_{2}\in Cl\left(\phi\right):\phi_{1}\textrm{R}\ph... ...phi_{2}\in s\vee\left(\phi_{2}\in s\wedge\phi_{1}\textrm{R}\phi_{2}\in t\right)$

Akzeptierende Zustände

Für jede Unterformel der Form $\psi\equiv\phi_{1}\textrm{U}\phi_{2}$ gibt es eine Akzeptanzmenge $F_{\psi}$ wie folgt:

• $F_{\psi}$ ist die Menge der Zustände, die $\phi_{2}$ oder $\neg\phi_{1}\textrm{R}\neg\phi_{2}$ enthalten

Kripke  $\rightarrow$ Büchi

 

• gegeben: $\mathcal{K}=\left(S,\rightarrow,r,AP,\nu\right)$
• gesucht: $\mathcal{B}_{\mathcal{K}}=\left(Q,\Sigma,\delta,q,F\right)$
• $F=Q=S$
• $\Sigma=2^{AP}$
• $\left(s,A,s'\right)\in\delta$ $\Leftrightarrow$ $s\rightarrow s'$ und $A=\left\{ p\in AP\vert s\in\nu\left(p\right)\right\}$
• $q=r$
• $\mathcal{K}\models\phi\Leftrightarrow\mathcal{L}\left(\mathcal{B_{K}}\right)\s... ...ow\mathcal{L}\left(\mathcal{B_{K}}\times\mathcal{B}_{\neg\phi}\right)=\emptyset$
  • $\mathcal{L}\neq\emptyset$ wenn Graph von $\ldots$ enthält als Kreise mit Enzustand drin die erreichbar vom Start sind

  SCC

  starke Zusammenhangskomponente heißt $S\subseteq Q$ gdw. für alle $q,q'\in S$ gilt $q\rightarrow^{*}q'$

  • SCC heitßt trivial wenn $\left\vert S\right\vert=1$ und für $q\in S$ gilt $q\nrightarrow q$
  • $\mathcal{L}\neq\emptyset$ wenn Graph von $\ldots$ nicht-trivial SCC enthält die erreichbar vom Start ist

Aktionen

$\mathcal{K}=\left(S,A,\rightarrow,r,AP,\nu\right)$

• $S,r,AP,\nu$ wie bei Kripkestruktur
• $A$ sei eine Menge von Aktionen
• $\rightarrow\subseteq S\times A\times S$
• Sei $\left(s,a,s'\right)\in\rightarrow$ deterministisch, so dass sich schreiben lässt $s'=a\left(s\right)$
• $enabled\left(s\right)=\left\{ a\vert\exists s':\left(s,a,s'\right)\in\rightarrow\right\}$

Unabhängigkeit

$I\subseteq A\times A$ heißt Unabhängigkeitsrelation für $\mathcal{K}$, falls

• $\forall a\in A:\left(a,a\right)\notin I$
• $\forall\left(a,b\right)\in I:\left(b,a\right)\in I$
• $\forall\left(a,b\right)\in I,s\in S:$ Aktiviertheit: $a,b\in enabled\left(s\right)\Rightarrow a\in enabled\left(b\left(s\right)\righ... ...right)\right)\wedge a\left(b\left(s\right)\right)=b\left(a\left(s\right)\right)$
• $a$ und $b$ heißen unabhängig, falls $\left(a,b\right)\in I$

stotter äquivalenz

sind zwei Abläufe einer Kripke Struktur $\sigma$ und $\rho$, falls es Sequenzen $0=i_{0}<i_{1}<i_{2}<\ldots$ und $0=j_{0}<j_{1}<j_{2}<\ldots$ gibt, so dass für alle $k\ge0$ gilt:
$\nu^{-1}\left(\sigma\left(i_{k}\right)\right)=\nu^{-1}\left(\sigma\left(i_{k}+1\right)\right)=\ldots\nu^{-1}\left(\sigma\left(i_{k+1}-1\right)\right)$
$=$
$\nu^{-1}\left(\rho\left(j_{k}\right)\right)=\nu^{-1}\left(\rho\left(j_{k}+1\right)\right)=\ldots\nu^{-1}\left(\rho\left(j_{k+1}-1\right)\right)$

• Eine LTL-Formel $\phi$ heißt stotter-invariant, gdw. für alle äquivalenten Abläufe $\sigma$ und $\rho$ gilt
  $$\sigma\models\phi\Leftrightarrow\rho\models\phi$$

• Alle Formeln der LTL Logik ohne den X-Operator sind stotter-invariant
• Zwei Kripke $\mathcal{K}$ und $\mathcal{K}'$ Strukturen heißen stotter-äquivalent gdw.
  • sie den gleichen Anfangszustand haben
  • für jeden Ablauf $\sigma$ in $\mathcal{K}$ es einen stotter-äquivalenten Ablauf $\rho$ in $\mathcal{K}'$ gibt und umgekehrt.
• Stotter-invariante Formeln können stotter-äquivalente Kripkestrukturen nicht unterscheiden

Sichtbarkeit

Eine Aktion $a$ heißt unsichtbar, falls für alle $s,s'\in S$ gilt: Falls $\left(s,a,s'\right)\in\rightarrow$, dann gilt $\nu^{-1}\left(s\right)=\nu^{-1}\left(s'\right)$.

Ample sets

$ample\left(s\right)\subseteq enabled\left(s\right)$ ist die Menge an Nachfolgerzuständen die tatsächlich überprüft werden muss, beim Testen auf Leerheit der Sprache. $\mathcal{K}$ wird also auf $\mathcal{K}_{R}$ reduziert.

• $C0$: $ample\left(s\right)=\emptyset$ $\Leftrightarrow$ $enabled\left(s\right)=\emptyset$
• $C1$: Auf jedem Pfad beginnend in $s$ in $\mathcal{K}$ gilt: keine Aktion, die von einer Aktion in $ample\left(s\right)$ abhängt, kann vor einer Aktion in $ample\left(s\right)$ ausgeführt werden.
  Eine Aktion $b$, die von einer Aktion $a\in ample\left(s\right)$ abhängt, d.h. $\left(a,b\right)\notin I$, kann erst nach der Ausführung einer Aktion $c\in ample\left(s\right)$ ausgeführt werden.
• $C2:$ Falls $ample\left(s\right)\subsetneq enabled\left(s\right)$, sind alle Aktionen in $ample\left(s\right)$ unsichtbar
• $C3$: Für alle Zyklen in $\mathcal{K}_{R}$gilt: falls $a\in enabled\left(s\right)$ für einen Zustand im Zyklus, dann $a\in ample\left(s'\right)$ für einen Zustand $s'$ im Zyklus