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 15.9 KB
Newer Older
Theo von Arx's avatar
Theo von Arx committed
1
2
3
%! TEX root = DES.tex

\section{Specification Models}
Theo von Arx's avatar
Theo von Arx committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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
\subsection{Binary Decision Diagrams (BDD)}
\subsubsection{Representation of Boolean Functions}
BDDs represent Boolean functions and can be used to describe sets of states
and transformation relations.  \\
Due to the unique representation of Boolean functions,
BDDs can be used to proof equivalence between Boolean functions or between sets of states.

\textbf{Concept:}\\
\begin{itemize}
	\item Data structure that allows to represent Boolean
		functions.
	\item The representation is unique for a given ordering of
		variables.
\end{itemize}
\textbf{Structure:}\\
\begin{itemize}
	\item BDDs contain “decision nodes” which are labeled with
		variable names.
	\item Edges are labeled with input values.
	\item Leaves are labeled with output values.
	\item BDDs are unique for a given ordering of variables, also called \textbf{Ordered Binary Decision Diagrams (OBDD)}.
\end{itemize}

\begin{figure}[H]
	\centering
	\includegraphics[width=0.5\columnwidth]{fig/bdd-representation.png}
\end{figure}

\subsubsection{Decomposition}
\begin{ftext}
BDDs are based on the Boole-Shanon-Decomposition:
	\begin{align}
f = \bar{x} \cdot f\bigg\rvert_{x=0} + x \cdot f\bigg\rvert_{x=1}
	\end{align}
\end{ftext}

\begin{figure}[H]
	\centering
	\includegraphics[width=0.3\columnwidth]{fig/bdd-decomposition.png}
\end{figure}

\subsubsection{Calculating with BDDs}
TODO
\subsubsection{Representation of Sets}
\begin{ftext}
In order to find a representation of a subset $A \subseteq E$, we binary  encode all elements $e \in E$ with $\sigma(e)$. Then the representation of a is given as:
\begin{align}
	a \in A \Leftrightarrow \psi_A(\sigma(a)) \text{ is true}
\end{align}
\end{ftext}

For convenience, we remove the binary encoding $\sigma(\cdot)$ in our notation.
The following properties hold:
\begin{align}
	c \in A \cap B 	& \quad \Leftrightarrow \quad  \psi_A(c)\cdot\psi_B(c)	\\
	c \in A \cup B 	& \quad \Leftrightarrow \quad  \psi_A(c)+\psi_B(c)	\\
	c \in A \setminus B 	& \quad \Leftrightarrow \quad  \psi_A(c) \cdot \overline{\psi_B(c)}	\\
	c \in E \setminus A 	& \quad \Leftrightarrow \quad  \overline{\psi_A(c)}
\end{align}

Theo von Arx's avatar
Theo von Arx committed
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
\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]
Theo von Arx's avatar
Theo von Arx committed
80
81
82
83
84
85
86
87
88
89
90
	\centering
	\begin{subfigure}[b]{0.4\columnwidth}
		\centering
		\includegraphics[width=\linewidth]{fig/state-or-super}
		\caption*{OR-super-state}
	\end{subfigure}
	\begin{subfigure}[b]{0.4\columnwidth}
		\centering
		\includegraphics[width=\linewidth]{fig/state-and-super}
		\caption*{AND-super-state}
	\end{subfigure}
Theo von Arx's avatar
Theo von Arx committed
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
\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.

Theo von Arx's avatar
Theo von Arx committed
112
113


Theo von Arx's avatar
Theo von Arx committed
114
115
116
117
118
119
120
121
\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}

Theo von Arx's avatar
Theo von Arx committed
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
\subsection{Reachability of States}
\paragraph*{Problem:} Is a state reachable by a sequence of state transitions?

\paragraph*{Method:}
\begin{itemize}
	\item Represent set of states and the transformation relation as OBDDs.
	\item Use these representations to transform set of sets. Set corresponds to the set of states reachable after $i$ transitions.
	\item Iterate the transformation until a fixed-point is reached, i.e., until the set of states does not change anymore (steady-state).
\end{itemize}

\paragraph*{Example:}
~
\begin{figure}[H]
	\centering
	\includegraphics[width=\columnwidth]{fig/reach-example.png}
\end{figure}

\subsubsection{Transformation of Sets of States}
Determine the set of all direct successor states of a given set of states $Q$ by means of the transformation function:
\begin{align}
	Q' &= \text{Suc}(Q, \delta) = \{ q' \vert ∃ q \text{ with } \psi_Q(q) \cdot \psi_\delta(q,q')\}\\
	\intertext{where}
	\psi_Q(q) = 1 &\Leftrightarrow q\in Q\\
	\psi_\delta(q,q') = 1& \Leftrightarrow \text{There exists a transition between } q \text{ and } q'
\end{align}


\subsubsection{Fixed-Point Iteration}
TODO
\subsubsection{Comparison of Finite Automatas}
We define the following characteristic functions for two automatas $A$ and $B$ with states $x_A$, $x_B$ and outputs $y_A= w(x_A)$, $y_B= w(x_B)$ respectively and the shared input $u$:
\begin{align}
	\intertext{transition function of $A$:} & ψ_r^A (x_A', x_A , u)\\
	\intertext{joint transition function:}  ψ_f (x_A , x_A' , x_B , x_B' ) = & (∃u : ψ_r^A (x_A , x_A' , u) \cdot ψ_r^B (x_B , x_B' , u))\\
	\intertext{joint function of reachable states:} & ψ_X (x_A , x_B) \\
	\intertext{joint function of reachable output:}
	ψ_Y (y_A , y_B) = &~(∃ x_A, x_B : \psi_X(x_A,x_B) \cdot  \psi_w^A(x_A, y_A) \cdot \psi_w^B(x_B, y_B)\\
\end{align}

\begin{fsatz}
	The automata are not equivalent iff the following term is true:
	\begin{align}
		∃ y_A,y_B~:~ \psi_Y(y_A, y_B)\cdot (y_A \neq y_B)
	\end{align}
\end{fsatz}

Theo von Arx's avatar
Theo von Arx committed
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

\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]
Theo von Arx's avatar
Theo von Arx committed
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
	\centering
	\begin{subfigure}[h]{0.3\columnwidth}
		\centering
		\includegraphics[scale=1.0]{fig/petri-source}
		\caption*{Token source}
	\end{subfigure}
	\begin{subfigure}[h]{0.3\columnwidth}
		\centering
		\includegraphics[scale=1.0]{fig/petri-sink}
		\caption*{Token sink}
	\end{subfigure}
	\begin{subfigure}[h]{0.3\columnwidth}
		\centering
		\includegraphics[scale=1.0]{fig/petri-selfloop}
		\caption*{Self-Loop}
	\end{subfigure}
Theo von Arx's avatar
Theo von Arx committed
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
\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}
Theo von Arx's avatar
Theo von Arx committed
272
	Jede reguläre Sprache ist auch eine Petri-Netz Sprache.
Theo von Arx's avatar
Theo von Arx committed
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
\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}
Theo von Arx's avatar
Theo von Arx committed
307
308
309
310
311
312
313
314
			\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}
Theo von Arx's avatar
Theo von Arx committed
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
		\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.
\[
Theo von Arx's avatar
Theo von Arx committed
337
	A_{ij} = \text{Gewinn der Tokens des Knotens $i \leq m$, wenn die Transition $j \leq n$ feuert}
Theo von Arx's avatar
Theo von Arx committed
338
339
340
341
342
343
344
345
346
347
348
349
350
351
\]

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
\[
Theo von Arx's avatar
Theo von Arx committed
352
	M_{k+1} = M_k + A \cdot u_i
Theo von Arx's avatar
Theo von Arx committed
353
354
355
356
357
\]
\\

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
\[
Theo von Arx's avatar
Theo von Arx committed
358
	M_k = M_0 + A \cdot \sum\limits_{i = 1}^{k} u_{\sigma[i]}
Theo von Arx's avatar
Theo von Arx committed
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
\]

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}