Skip to content
Snippets Groups Projects
Commit 859197e4 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

add image link

parent fd05bef9
Branches
No related tags found
No related merge requests found
%% Cell type:markdown id: tags:
## Endliche Automaten : DFA
Jede Klasse der Chomsky-Hierarchie kann durch einen geeigneten Automatentypen charakterisiert
werden. Beispielsweise kann jede reguläre Sprache (Typ 3) durch einen endlichen Automaten
erkannt werden, und jede von einem endlichen Automaten erkannte Sprache ist
regulär.
Endliche Automaten sind weit verbreitet. Ein Beispiel ist die Spezifikation des [DHCP Protokolls](http://www.tcpipguide.com/free/t_DHCPGeneralOperationandClientFiniteStateMachine.htm#Figure_262):
<img src="http://www.tcpipguide.com/free/diagrams/dhcpfsm.png" width="500"/>
%% Cell type:markdown id: tags:
### DFA
Ein __deterministischer endlicher Automat__ (kurz DFA für
deterministic finite automaton) ist ein Quintupel
$M =(\Sigma, Z, \delta , z_0, F)$, wobei
* $\Sigma$ ein Alphabet ist,
* $Z$ eine endliche Menge von Zuständen mit
$\Sigma \cap Z = \emptyset$,
* $\delta : Z \times \Sigma \rightarrow Z$ die Überführungsfunktion,
* $z_0 \in Z$ der Startzustand und
* $F \subseteq Z$ die Menge der Endzustände (Finalzustände).
%% Cell type:code id: tags:
``` prob
::load
MACHINE DFA
SETS
Z = {z0,z1,z2,z3}
CONSTANTS Σ, F, δ
PROPERTIES
F ⊆ Z ∧
δ ∈ (Z×Σ) → Z
/* Der Automat von Folie 10: */
Σ = {0,1} ∧
F={z2} ∧
δ = { (z0,0)↦z1, (z0,1)↦z3,
(z1,0)↦z3, (z1,1)↦z2,
(z2,0)↦z2, (z2,1)↦z2,
(z3,0)↦z3, (z3,1)↦z3 }
DEFINITIONS
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F);
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F);
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{a,b|(a,0)|->b:δ});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{a,b|(a,1)|->b:δ});
CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0})
END
```
%% Output
Loaded machine: DFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags:
Ein Automat befindet sich jeweils in einem der Zustände $z$ aus Z. Er kann dann in diesem Zustand ein Symbol $x$ aus $\Sigma$ verarbeiten und wechselt dann in den Zustand $\delta(z,x)$.
Zum Beispiel, wenn der DFA im Zustand z0 das Symbol $0$ erhält wechselt er nach:
%% Cell type:code id: tags:
``` prob
δ(z0,0)
```
%% Output
$\mathit{z1}$
z1
%% Cell type:markdown id: tags:
Wenn der Automat dann das Symbol 1 erhält wechselt er von Zustand $z1$ nach:
%% Cell type:code id: tags:
``` prob
δ(z1,1)
```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags:
Da $z2\in F$ ein Endzustand ist, akzeptiert der DFA das Wort $01$ (oder $[0,1]$ in der Notation vom Notebook).
%% Cell type:markdown id: tags:
#### Zustandgraph
Man kann den DFA auch grafisch darstellen: Endzustände sind mit einem doppelten Kreis gekennzeichnet, der Anfangszustand wird durch eine besondere Startkante gekennzeichnet.
Formal ist dies so definiert:
Ein DFA $M= (\Sigma, Z, \delta , z_0, F)$ lässt sich anschaulich durch
seinen __Zustandsgraphen__ darstellen,
\begin{itemize}
* dessen Knoten die Zustände von $M$ und
* dessen Kanten Zustands"uberg"ange gemäß der
Überführungs\-funktion $\delta$ repräsentieren.
* Gilt $\delta(z,a) = z'$ f"ur ein Symbol $a \in \Sigma$ und für
zwei Zustände $z, z' \in Z$, so hat dieser Graph eine gerichtete
Kante von $z$ nach~$z'$, die mit $a$ beschriftet ist.
* Der Startzustand wird durch einen Pfeil auf $z_0$ dargestellt.
* Endzustände sind durch einen Doppelkreis markiert.
Für den Automaten oben ergiebt dies folgenden Zustandsgraphen.
(Anmerkung: diese Darstellung erfordert eine neue Version des Jupyter-Kernels. Falls diese bei ihnen nicht funktioniert schauen Sie sich die Abbildung auf den Folien an).
%% Cell type:code id: tags:
``` prob
:dot custom_graph
```
%% Output
<Dot visualization: custom_graph []>
%% Cell type:markdown id: tags:
#### Erweiterte Überführungsfunktion und akzeptierte Sprache
Wir hatten gesehen, dass der Automat von $z0$ bei der Eingabe von $0$ nach $z1=\delta(z0,0)$
wechselt und nach einer weiteren Eingabe von $1$ in den Zustand $z2 = \delta(z1,1)$ wechselt.
Den aktuellen Zustand nach der Eingabe von dem Wort $01$ kann man also so berechnen:
%% Cell type:code id: tags:
``` prob
δ(δ(z0,0),1)
```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags:
Dies führt zu der folgenden Definition, mit der man den Zustand nach einer beliebigen Folge von Eingabesymbolen berechnen kann:
Sei $M = (\Sigma, Z, \delta , z_0, F)$ ein DFA.
Die __erweiterte Überführungsfunktion
$\widehat{\delta} : Z \times \Sigma^* \rightarrow Z$ von $M$ ist induktiv definiert:
* ${\delta}(z, \lambda) = z$
* ${\delta}(z, ax) = \widehat{\delta}(\delta(z,a), x) $
für alle $z \in Z$, $a \in \Sigma$ und $x \in \Sigma^*$.
Die vom DFA $M$ __akzeptierte Sprache__ ist definiert durch
* $L(M) = \{w \in \Sigma^* \Longleftrightarrow \widehat{\delta}(z_0,w) \in F\}$
Diese Definitionen sind in der folgenden B Maschine umgesetzt.
$\widehat{\delta}$ wird durch die rekursive Funktion $\delta s$ dargestellt.
%% Cell type:code id: tags:
``` prob
::load
MACHINE DFA
SETS
Z = {z0,z1,z2,z3}
ABSTRACT_CONSTANTS δs, L
CONSTANTS Σ, F, δ
PROPERTIES
F ⊆ Z ∧ δ ∈ (Z×Σ) → Z ∧
/* Definition der erweiterten Überführungsfunktion */
δs ∈ (Z×seq(Σ)) → Z ∧
δs = λ(z,s).(z∈Z ∧ s∈seq(Σ) |
IF s=[] THEN z
ELSE δs(δ(z,first(s)),tail(s)) END)
/* Die vom Automaten akzeptierte Sprache L */
L = {ω|ω∈seq(Σ) ∧ δs(z0,ω) ∈ F}
/* Der Automat von Folie 10: */
Σ = {0,1} ∧
F = {z2} ∧
δ = { (z0,0)↦z1, (z0,1)↦z3,
(z1,0)↦z3, (z1,1)↦z2,
(z2,0)↦z2, (z2,1)↦z2,
(z3,0)↦z3, (z3,1)↦z3 }
DEFINITIONS
CUSTOM_GRAPH_NODES1 == rec(shape:"doublecircle",nodes:F);
CUSTOM_GRAPH_NODES2 == rec(shape:"circle",nodes:Z\F);
CUSTOM_GRAPH_NODES3 == rec(shape:"none",color:"white",style:"none",nodes:{""});
CUSTOM_GRAPH_EDGES1 == rec(color:"red",label:"0",edges:{a,b|(a,0)|->b:δ});
CUSTOM_GRAPH_EDGES2 == rec(color:"green",label:"1",edges:{a,b|(a,1)|->b:δ});
CUSTOM_GRAPH_EDGES3 == rec(color:"black",label:"",edges:{"" |-> z0})
END
```
%% Output
Loaded machine: DFA
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:markdown id: tags:
Man kann mit der erweiterten Überführungsfunktion den Zustand nach der Eingabe [0,1] so bestimmen:
%% Cell type:code id: tags:
``` prob
δs(z0,[0,1])
```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags:
Da $z0\in F$ gilt:
%% Cell type:code id: tags:
``` prob
[0,1] ∈ L
```
%% Output
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
δs(z0,[1,0])
```
%% Output
$\mathit{z3}$
z3
%% Cell type:markdown id: tags:
Da $z3\not\in F$
%% Cell type:code id: tags:
``` prob
[1,0] ∈ L
```
%% Output
$\mathit{FALSE}$
FALSE
%% Cell type:markdown id: tags:
Hier sind die Wörter der Länge 3 und 4 die vom DFA akzeptiert werden:
%% Cell type:code id: tags:
``` prob
:table {w1,w2,w3| [w1,w2,w3] : L}
```
%% Output
|w1|w2|w3|
|---|---|---|
|$0$|$1$|$0$|
|$0$|$1$|$1$|
w1 w2 w3
0 1 0
0 1 1
%% Cell type:code id: tags:
``` prob
:table {w1,w2,w3,w4| [w1,w2,w3,w4] : L}
```
%% Output
|w1|w2|w3|w4|
|---|---|---|---|
|$0$|$1$|$0$|$0$|
|$0$|$1$|$0$|$1$|
|$0$|$1$|$1$|$0$|
|$0$|$1$|$1$|$1$|
w1 w2 w3 w4
0 1 0 0
0 1 0 1
0 1 1 0
0 1 1 1
%% Cell type:markdown id: tags:
Anmerkung:
Für $a \in \Sigma$ gilt $\widehat{\delta}(z, a) = \delta(z, a)$, und
\item für $x = a_1 a_2 \cdots a_n$ in $\Sigma^*$ gilt:
* $\widehat{\delta}(z, x) = \delta( \cdots \delta(\delta(z, a_1), a_2)\cdots , a_n).$
Zum Beispiel:
%% Cell type:code id: tags:
``` prob
δs(z0,[0,1,1,1])
```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags:
ist identisch zu:
%% Cell type:code id: tags:
``` prob
δ(δ(δ(δ(z0,0),1),1),1)
```
%% Output
$\mathit{z2}$
z2
%% Cell type:markdown id: tags:
Was man schrittweise ausrechnen kann:
%% Cell type:code id: tags:
``` prob
δ(δ(δ(z1,1),1),1)
```
%% Output
$\mathit{z2}$
z2
%% Cell type:code id: tags:
``` prob
δ(δ(z2,1),1)
```
%% Output
$\mathit{z2}$
z2
%% Cell type:code id: tags:
``` prob
δ(z2,1)
```
%% Output
$\mathit{z2}$
z2
%% Cell type:code id: tags:
``` prob
```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment