Zustand aus einem GNEA entfernen

Einfache Sprache

Def. Satz Zustand aus einem GNEA entfernen

Sei $\mathcal A$ ein GNEA und $q\in Q$ mit $q\not\in\{q_I,q_F\}$. Der zu $\mathcal A$ Äquivalente Automaten ohne den Zustand $q$ ist der GNEA $\mathcal A-q = (Q',A,q_I,q_F,\delta')$, wobei

• $Q' = Q\setminus\{q\}$,
• $\forall p\in Q'\setminus\{q_F\},p'\in Q'\setminus\{q_I\}:\delta'(p,p') = \delta(p,p')|\delta(p,q)\delta(q,q)^*\delta(q,p')$

Beweis: Nach der Definition von Äquivalenz müssen wir zeigen, dass $L(\mathcal A) = L(\mathcal A- q)$. Wir zeigen es durch beidseitige Inklusion:

“$\subseteq$”: Wir nutzen Induktion über die $q$-länge, die wir jetzt definieren:

Ein partielle $q$-Berechnung von $\mathcal A$ auf einem Wort $u$ ist eine Liste von Zuständen $q_0\ldots q_n$ so, dass

• $u = u_0\ldots u_{n-1}$,
• $q_0 = q_I$,
• $\forall i\in [1,n-1]:q_i\in Q\setminus\{q_I,q_F\}$,
• $\forall n\in[1,n]:q_n\in Q\setminus\{q_I,q\}$ und
• $\forall i\in [0,n-1]:u_i\in L(\delta(q_i,q_{i+1}))$.

Analog zu Satz Zustand aus einem GNEA entfernen wird hier auch $\mathcal A - q$ definiert.

Wir zeigen nun folgendes: Falls ein partielle $q$-Berechnung von $\mathcal A$ auf $u$ exisitiert, der mit $q'\not=q$ endet, dann existiert eine partielle $q$-Berechnung von $\mathcal A - q$ auf $u$.

Für eine Liste von Zuständen $q_0\ldots q_n$ definieren wir die $q$-länge $|\cdot|_q$ wie folgt

Wir machen nun eine Induktion über die $q$-Länge.

IA: Sei $|q_0\ldots q_n|_q = 1$. Dann muss $q_0\ldots q_n = q_0 = q_I$ gelten. Da wir nur in einem Zustand sind und nicht wechseln ist das Wort $u$ da leere Wort, also $u = \varepsilon$. Diese partielle $q$-Berechnung existiert genau so auch bei $\mathcal A-q$ auf $\varepsilon$.

IS: Sei $|q_0\ldots q_n|_q = m+1$ mit $m > 0$. Dann kann $q_0\ldots q_n$ als $q_0\ldots q_{n_0}q^rq_n$ geschrieben werden, wobei $q_{n_0} \not=q$ und $q_n\not= q$. Wir nehmen an (IH), dass eine partielle $q$-Berechnung von $\mathcal A-q$ auf $u_0\ldots u_{n-1}$ die auf $q_{n_0}$ endet, wir geben dieser Berechnung die Zustände $q_0'\ldots q_{n'}'$. Abhängig von $r$ erweitern wir die partielle $q$-Berechnung von $\mathcal A-q$ um den Zustand $q_n$.

FÜr den Korrektheitsbeweis machen wir eine Fallunterscheidung über $r$.

Falls $r = 0$, dann gilt

Sonst $r > 0$, dann gilt

“$\supseteq$”: #TODO