Theo von Arx committed Jan 14, 2019 1 2 3 %! TEX root = DES.tex \section{Specification Models}  Theo von Arx committed Jan 14, 2019 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 committed Jan 14, 2019 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 committed Jan 14, 2019 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 committed Jan 14, 2019 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 committed Jan 14, 2019 112 113   Theo von Arx committed Jan 14, 2019 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 committed Jan 14, 2019 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 committed Jan 14, 2019 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 committed Jan 14, 2019 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 committed Jan 14, 2019 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 committed Jan 14, 2019 272  Jede reguläre Sprache ist auch eine Petri-Netz Sprache.  Theo von Arx committed Jan 14, 2019 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 committed Jan 14, 2019 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 committed Jan 14, 2019 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 committed Jan 14, 2019 337  A_{ij} = \text{Gewinn der Tokens des Knotens i \leq m, wenn die Transition j \leq n feuert}  Theo von Arx committed Jan 14, 2019 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 committed Jan 14, 2019 352  M_{k+1} = M_k + A \cdot u_i  Theo von Arx committed Jan 14, 2019 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 committed Jan 14, 2019 358  M_k = M_0 + A \cdot \sum\limits_{i = 1}^{k} u_{\sigma[i]}  Theo von Arx committed Jan 14, 2019 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}