Commit 45daac58 authored by Theo von Arx's avatar Theo von Arx

Add Binary Decision Diagrams

parent 21accef6
%! 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.
......@@ -17,17 +77,17 @@ Ein Super-State wird OR-Super-State genannt, wenn genau ein Sub-State aktiv ist,
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}
\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}
......@@ -83,22 +143,22 @@ 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}
\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.
......@@ -161,7 +221,7 @@ Man sagt, dass das Petri-Netz $P$ einen String $w$ genau dann akzeptiert, wenn e
Jeder endlicher Automat kann als Petri-Netz dargestellt werden.
\begin{ftext}
Jede reguläre Sprache ist auch eine Petri-Netz Sprache.
Jede reguläre Sprache ist auch eine Petri-Netz Sprache.
\end{ftext}
\subsubsection{Eigenschaften}
......@@ -195,16 +255,16 @@ 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.
\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}
\end{itemize}
\begin{figure}[H]
......@@ -226,7 +286,7 @@ Für bounded Petri-Netze enthält der Baum keine $\omega$ und wird auch Reachabi
\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}
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.
......@@ -241,13 +301,13 @@ Ein Feuerungsvektor $u$ beschreibt das Feuern der Transition $t_i$. Er besteht a
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
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]}
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).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment