%! TEX root = DES.tex \section{Specification Models} \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} \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 \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} \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{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} \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 \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} \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}