Commit ffb3f8d9 authored by zrene's avatar zrene
parents e21fdd80 2156f1be
......@@ -265,3 +265,4 @@
\newcommand{\C}{\mathbb{C}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\tA}{\mathbb{A}}
......@@ -147,15 +147,27 @@ Determine the set of all direct successor states of a given set of states $Q$ by
\subsubsection{Fixed-Point Iteration}
TODO
Starte mit dem Initialzustand und bestimme die Menge der innert einem oder mehreren Schritten
erreichbaren Zustände.
\begin{align}
Q_0 &= \{q_0\}\\
Q_{i+1} &= Q_i \cup \{ q' | ∃ q \text{with } \psi_Q(q) \cdot \psi_\delta(q,q')\}\\
\shortintertext{oder}
\psi_{Q_{i+1}}(q') &= \psi_{Q_i}(q) + (∃q : \psi_{Q_i}(q) \cdot \psi_\delta (q, q'))\\
\intertext{wiederhole den Iteratiosschritt solange, bis gilt:}
Q_{i+1} &= Q_i =: \hat{Q}
\end{align}
Dann beschreibt $\hat{Q}$ die Menge aller erreichbaren Zustände.
\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)\\
ψ_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}
......@@ -165,7 +177,34 @@ We define the following characteristic functions for two automatas $A$ and $B$ w
\end{align}
\end{fsatz}
\subsection{Computation Tree Logic (CTL)}
\begin{fdef}
Sei $\phi$ eine Eigenschaft eines Systems. Dann definieren wir:
\begin{align}
\text{E}\phi :\quad& \text{There exists at least one path from the current}\\
& \text{state where $\phi$ holds.}\\
\text{X}\phi :\quad &\text{$\phi$ has to hold at the next state.}\\
\text{G}\phi :\quad & \text{$\phi$ has to hold on the entire subsequent path.}\\
\phi_1 \text{U}\phi_2 :\quad & \text{$\phi_1$ has to hold at least until at some state $\phi_2$ holds.}
\end{align}
\end{fdef}
\begin{fsatz}
There are more quantifiers, but they can be replaced by the above ones:
\begin{align}
\text{F} \phi :\quad & \text{$\phi$ eventually has to hold (somewhere on the subsequent path).}\\
\text{A} \phi :\quad & \text{$\phi$ has to hold on all paths starting from the current state.}
\end{align}
\end{fsatz}
\subsubsection{Beispiele}
Zustand ist schwarz $\equiv$ Eigenschaft $p$ ist erfüllt.\\
Zustand ist rot $\equiv$ Eigenschaft $q$ ist erfüllt.\\
\includegraphics[width=\columnwidth]{fig/ctl-agp.png}
\includegraphics[width=\columnwidth]{fig/ctl-axp.png}
\includegraphics[width=\columnwidth]{fig/ctl-egp.png}
\includegraphics[width=\columnwidth]{fig/ctl-exp.png}
\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.
......
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