To receive notifications about scheduled maintenance, please subscribe to the mailing-list gitlab-operations@sympa.ethz.ch. You can subscribe to the mailing-list at https://sympa.ethz.ch

specificationModels.tex 12.2 KB
Newer Older
Theo von Arx's avatar
Theo von Arx committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
%! TEX root = DES.tex

\section{Specification Models}
\subsection{State Charts}
In einem endlichen Automaten läuft immer genau ein Prozess sequentiell ab, es gibt keine Parallelität. Ausserdem gibt es keinerlei hierarchische Strukturen.\\
State Charts beheben diese Probleme indem sie Super-States einführen, deren Zustände selbst wieder Super-States sein können. Zustände, die nicht aus anderen Zuständen zusammengesetzt sind (keine Super-states), nennt man Basis-Zustände.

\begin{figure}[H]
	\centering
	\includegraphics[width=\columnwidth]{fig/state-super}
\end{figure}

\paragraph*{OR-Super-State}
Ein Super-State wird OR-Super-State genannt, wenn genau ein Sub-State aktiv ist, wenn S aktiv ist.

\paragraph*{AND-Super-State}
Ein Super-State wird AND-Super-State genannt, wenn alle direkten Sub-States aktiv sind, wenn S aktiv ist.

\begin{figure}[H]
        \centering
Theo von Arx's avatar
Theo von Arx committed
21
        \begin{subfigure}[b]{0.4\columnwidth}
Theo von Arx's avatar
Theo von Arx committed
22
                \centering
Theo von Arx's avatar
Theo von Arx committed
23
                \includegraphics[width=\linewidth]{fig/state-or-super}
Theo von Arx's avatar
Theo von Arx committed
24
25
                \caption*{OR-super-state}
        \end{subfigure}
Theo von Arx's avatar
Theo von Arx committed
26
        \begin{subfigure}[b]{0.4\columnwidth}
Theo von Arx's avatar
Theo von Arx committed
27
                \centering
Theo von Arx's avatar
Theo von Arx committed
28
                \includegraphics[width=\linewidth]{fig/state-and-super}
Theo von Arx's avatar
Theo von Arx committed
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
                \caption*{AND-super-state}
        \end{subfigure}
\end{figure}

\paragraph*{Event}
Ein Event kann entweder intern (vom State Chart) oder extern generiert werden. Es können Events kombiniert werden wie (E1 and E2), (E1 or E2) oder (not E).

\paragraph*{Condition}
Eine Bedingung bezieht sich auf den Wert von Variablen. Bedingungen können wie Events kombiniert werden.

\paragraph*{Zustandsübergang}
Der Übergang ist aktiv, wenn der Event existiert und die Bedingung erfüllt ist

\paragraph*{Reaction / Aktion}
Beim Zustandsübergang können Variablen neue Werte zugewiesen oder Events generiert werden. Reaktionen können sequentiell ausgeführt werden mit (A1; A2).

\begin{figure}[H]
	\centering
	\includegraphics[scale=0.4]{fig/state-events}
\end{figure}

Alle Events, Zustände und Aktionen sind global sichtbar.

\subsubsection{Simulation}
State Charts werden in drei Phasen simuliert:
\begin{enumerate}
	\item Auswirkungen von Veränderungen der Events und Bedingungen werden ausgewertet.
	\item Die Menge der Zustandsübergänge, die in diesem Schritt gemacht werden müssen und die rechte Seite von Zuweisungen wird berechnet.
	\item Übergänge werden durchgeführt, Variablen erhalten ihren neuen Wert.
\end{enumerate}


\subsection{Petri-Netze}
Im Gegensatz zu hierarchischen State Maschinen (State Charts), Zustandsübergange in einem Petri-Netz sind asynchron. Die Reihenfolge der Übergänge ist zum Teil unkoordiniert. Sie ist gegeben durch eine Teilreihenfolge. \\
Petri-Netze können deshalb dafür benutzt werden verteilte gleichzeitige Prozesse zu modellieren.
\\

Definition: Ein Petri-Netz ist ein bipartiter, gerichteter Graph definiert durch einen 4-Tuple $(S, T, F, M_0)$ mit
\begin{itemize}
	\item $S$ ist eine Menge von Plätzen $p_i$
	\item $T$ ist eine Menge von Transitionen $t_i$
	\item $F$ ist eine Menge von Kanten (Flussverhältnissen) $f_i$
	\item $M_0: S \to \mathbb{N}$ ist die anfängliche Verteilung der Tokens
\end{itemize}

\begin{figure}[H]
	\centering
	\includegraphics[width=\columnwidth]{fig/petri-fire}
\end{figure}


Eine Markierung $M$ aktiviert eine Transition $t \in T$, wenn in jedem Eingangsplatz $p_i$ mindestens ein Token liegt. \\
Wenn die Transition aktiviert ist, so wird diese feuern und von der Markierung $M$ zur Markierung $M\prime$ übergehen.(schlussendlich). \\
Nur eine Transition feuert zu einer gegebenen Zeit. \\
Wenn eine Transition feuert, so verbraucht so bei jedem ihrer Eigangsplätze ein Token und fügt jedem ihrer Ausgangsplätze ein Token hinzu.

\begin{figure}[H]
        \centering
Theo von Arx's avatar
Theo von Arx committed
87
        \begin{subfigure}[h]{0.3\columnwidth}
Theo von Arx's avatar
Theo von Arx committed
88
89
90
91
                \centering
                \includegraphics[scale=1.0]{fig/petri-source}
                \caption*{Token source}
        \end{subfigure}
Theo von Arx's avatar
Theo von Arx committed
92
        \begin{subfigure}[h]{0.3\columnwidth}
Theo von Arx's avatar
Theo von Arx committed
93
94
95
96
                \centering
                \includegraphics[scale=1.0]{fig/petri-sink}
                \caption*{Token sink}
        \end{subfigure}
Theo von Arx's avatar
Theo von Arx committed
97
        \begin{subfigure}[h]{0.3\columnwidth}
Theo von Arx's avatar
Theo von Arx committed
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
                \centering
                \includegraphics[scale=1.0]{fig/petri-selfloop}
                \caption*{Self-Loop}
        \end{subfigure}
\end{figure}

Petri-Netze sind nicht nicht deterministisch.
\\

\subparagraph{Pre-Set} $\bullet t := \{ p \, | \, (p, t) \in F \}$ und $p \in S$, $t \in T$

\subparagraph{Post-Set} $t \bullet = \{ p \, | \, (t, p) \in F \}$ und $p \in S$, $t \in T$

\subsubsection{Gewichtete Kanten}
Einer Kante kann ein Gewicht $k$ zugewiesen werden. Eine Transition benötigt dann $k$ Tokens von einem Platz, falls es eine Eingangskante ist. Die Transition fügt $k$ Tokens hinzu falls es eine Ausgangskante ist.

\begin{figure}[H]
	\centering
	\includegraphics[scale=1.0]{fig/petri-weighted}
\end{figure}



\subsubsection{Kapazitätsbeschränkungen}
Jeder Platz kann maximal $K(p_i)$ Tokens enthalten. Eine Transition $t$ ist nur aktiv, falls alle Ausgangsplätze von $t$ nach dem Feuern ihre Kapazität $K(p_i)$ nicht überschreiten.

\paragraph*{Kapazitätsbeschränkungen entfernen}
Pure (d.h. ohne self-loops) Petri-Netze mit Kapazitätsbeschränkungen können in äquivalente Petri-Netze ohne Kapazitätsbeschränkungen transformiert werden.
\\

Vorgehen:
\begin{itemize}
	\item Für jeden Platz mit $K(p) > 1$, füge einen Komplementärplatz $p^\prime$ mit Anfangsmarkierung $M_0 (p^\prime) = K(p) - M_0 (p)$ hinzu.
	\item Für jede ausgehende Kante $e = (p, t)$, füge eine Kante $e^\prime$ von $t$ zu $p^\prime$ mit Gewicht $W(e)$ hinzu.
	\item Für jede eingehende Kante $e = (t, p)$, füge eine Kante $e^\prime$ von $p^\prime$ zu $t$ mit Gewicht $W(e)$ hinzu.
\end{itemize}

\begin{figure}[H]
	\centering
	\includegraphics[width=\columnwidth]{fig/petri-capacity}
\end{figure}

Der Komplementärplatz $p^\prime$ hat als Anzahl Tokens, die noch verbleibende Kapazität von $p$.

\subsubsection{Self-Loops entfernen}
\begin{figure}[H]
	\centering
	\includegraphics[width=\columnwidth]{fig/petri-selfloop-remove}
\end{figure}


\subsubsection{Petri-Netz Sprachen}
Transitionen werden mit (nicht notwendigerweise verschiedenen) Symbolen beschriftet. Jede Sequenz von Transitions-Feuerungen generiert einen String von Symbolen.
\\

Man sagt, dass das Petri-Netz $P$ einen String $w$ genau dann akzeptiert, wenn es eine gültige Feuerungssequenz $\sigma_w$ für $w$ gibt und das Petri-Netz dead is nach der Ausführung von $\sigma_w$.

\begin{figure}[H]
	\centering
	\includegraphics[scale=0.4]{fig/petri-lang-bsp}
	\caption*{Petri-Netz für die Sprache $L = \{ 0^a 1^a \, | \, a \geq 0 \}$}
\end{figure}

Jeder endlicher Automat kann als Petri-Netz dargestellt werden.

\begin{ftext}
Jede reguläre Sprache ist auch eine Petri-Netz Sprache.
\end{ftext}

\subsubsection{Eigenschaften}
\paragraph*{Erreichbarkeit (Reachability)} Eine Markierung $M_n$ ist erreichbar, wenn eine Sequenz von Feuerungen $\{ t_1, t_2, \ldots, t_n \}$ existiert, so dass $M_n = M_0 \cdot t_1 \cdot t_2 \cdots t_n$.

\paragraph*{K-Boundedness} Ein Petri-Netz ist $K-bounded$, wenn die Anzahl Tokens in jedem Platz $K$ nie übersteigt. $\Rightarrow$ Die Anzahl der Zustände ist endlich.

\paragraph*{Safety} 1-Boundedness: Jeder Platz hält zu jeder Zeit maximum 1 Token.

\paragraph*{Liveness}
Eine Transition $t$ in einem Petri-Netz ist
\begin{itemize}
	\item \textbf{dead}: Genau dann, wenn $t$ in keiner Feuerungssequenz $L(M_0)$ feuern kann.
	\item \textbf{$L_1$-live}: Genau dann, wenn $t$ mindestens einmal in einer Sequenz $L(M_0)$ gefeuert werden kann.
	\item \textbf{$L_2$-live}: Genau dann, wenn $\forall k \in \mathbb{N}^+$, $t$ mindestens $k$ mal gefeuert werden kann in einer Sequenz $L(M_0)$.
	\item \textbf{$L_3$-live}: Genau dann, wenn $t$ unbegrenzt oft in einer unendlichen Sequenz $L(M_0)$ vorkommt.
	\item \textbf{$L_4$-live} (Live): Genau dann, wenn $t$ $L_1$-live für jede mögliche Markierung, die von $M_0$ erreichbar ist.
\end{itemize}
Es gilt: $L_4$-liveness $\Rightarrow$ $L_3$-liveness $\Rightarrow$ $L_2$-liveness $\Rightarrow$ $L_1$-liveness
\\

Die Liveness-Eigenschaft gilt analog für ganze Petri-Netze, wenn die Eigenschaft für alle Transition im Netz gilt.


\subsubsection{Analyse-Methoden: Coverability Tree}
Wir wollen herausfinden welche Token Verteilungen erreichbar sind. Da es möglicherweise unendlich viele gibt, müssen wir einen unendlichen Baum verhindern. \\
Wir benutzen das spezielle Symbol $\omega$ um eine beliebige Anzahl von Tokens zu markieren.
\\

Vorgehen:
\begin{itemize}
	\item Betrachte die Anfangsmarkierung $M_0$ als Stamm des Baumes und markiere sie als neu.
	\item Wiederhole, solange eine neue Markierung existiert: Wähle eine Markierung $M$ aus
	\begin{itemize}
		\item Falls $M$ identisch ist zu einer Markierung auf dem Weg vom Stamm zu $M$, markiere sie als alt
		\item Falls in $M$ keine Transitionen aktiviert sind, markiere $M$ als deadend.
		\item Für jede aktivierte Transition $t$ von $M$ mache
		\begin{itemize}
			\item Berechne Markierung $M^\prime = M \cdot $
			\item Falls eine Markierung $M^{\prime\prime}$ auf dem Weg vom Stamm zu $M$ existiert, so dass $M^\prime(p) \geq M^{\prime\prime}(p)$ für jeden Platz $p$ und $M^\prime \neq M^{\prime\prime}$, ersetze $M^\prime(p)$ mit $\omega$ für $p$ mit $M^\prime(p) > M^{\prime\prime}(p)$.
			\item Betrachte $M^\prime$ als neuen Knoten, zeichne ein Pfeil mit Label $t$ von $M$ zu $M^\prime$ und markiere $M^\prime$ als neu.
		\end{itemize}
	\end{itemize}
\end{itemize}

\begin{figure}[H]
	\centering
	\includegraphics[width=\columnwidth]{fig/petri-coverability}
\end{figure}

Resultate:
\begin{itemize}
	\item Das Netz ist bounded genau dann, wenn $\omega$ in keinem Label des Baumes auftaucht.
	\item Das Netz ist safe genau dann, wenn nur '0' und '1' in den Labels des Baumes auftauchen.
	\item Eine Transition ist dead genau dann, wenn sie in keinem Pfeil im Baum auftaucht.
	\item Wenn $M$ reachable ist von $M_0$ aus, dann existiert ein Knoten $M^\prime$, so dass $M \leq M^\prime$. (Das ist eine notwendige, aber nicht hinreichende Bedingungen für reachability).
\end{itemize}

Für bounded Petri-Netze enthält der Baum keine $\omega$ und wird auch Reachability Tree genannt, da er alle Markierungen enthält, die erreichbar sind.


\subsubsection{Analyse-Methoden: Incidence Matrix}
Die incidence Matrix $A$ $(m \times n)$ beschreibt den Tokenfluss anhand der $n$ verschiedenen Transitionen.
\[
A_{ij} = \text{Gewinn der Tokens des Knotens $i \leq m$, wenn die Transition $j \leq n$ feuert}
\]

Eine Markierung $M$ wird geschrieben als $m \times 1$ Spalten-Vektor.

\begin{figure}[H]
	\centering
	\includegraphics[width=\columnwidth]{fig/petri-incidence}
\end{figure}

Ein Feuerungsvektor $u$ beschreibt das Feuern der Transition $t_i$. Er besteht aus '0'en ausser in der $i$ten Spalte, wo er eine '1' hat. $u = (0, \ldots, 1, \ldots, 0)^T$
\\

Eine Transition $t_i$, die $M_k$ zu $M_{k+1}$ überführt kann geschrieben werden als
\[
M_{k+1} = M_k + A \cdot u_i
\]
\\

Eine Markierung $M_k$ ist reachable von $M_0$ aus, wenn eine Sequenz $\sigma$ von $k$ Transitionen $\{ t_{\sigma[1]}, t_{\sigma[2]}, \ldots, t_{\sigma[k]} \}$ existiert, für die gilt
\[
M_k = M_0 + A \cdot \sum\limits_{i = 1}^{k} u_{\sigma[i]}
\]

Das führt uns auf $M_k - M_0 = \Delta M = A \cdot \vec{x}$. Falls $M_k$ reachable ist von $M_0$, so muss diese Gleichung eine Lösung geben, bei der alle Komponenten von $\vec{x}$ positive Integers sind. (Das ist eine notwendige, aber nicht hinreichende Bedingungen für reachability).



\subsubsection{Analyse-Methoden: Vereinfachungsregeln}
Wir können Petri-Netze vereinfachen ohne folgende Eigenschaften zu verlieren: Liveness, Safeness, Boundedness
\\

Dazu können wir folgende Regeln verwenden:
\begin{figure}[H]
	\centering
	\includegraphics[width=\columnwidth]{fig/petri-reduction1}
\end{figure}
\begin{figure}[H]
	\centering
	\includegraphics[width=\columnwidth]{fig/petri-reduction2}
\end{figure}

\subsubsection{Inhibitor Arcs}
Ein Inhibitor Arc aktiviert eine Transition, wenn ein Platz keine Tokens enthält. \\
Petri Netze mit Inhibitor Arcs können nicht in normale Petri Netze umgewandelt werden.

\begin{figure}[H]
	\centering
	\includegraphics[width=\columnwidth]{fig/petri-inhibitor}
\end{figure}