Commit 97609f67 authored by Theo von Arx's avatar Theo von Arx

Improve Reachability of States

parent 45daac58
......@@ -109,6 +109,8 @@ Beim Zustandsübergang können Variablen neue Werte zugewiesen oder Events gener
Alle Events, Zustände und Aktionen sind global sichtbar.
\subsubsection{Simulation}
State Charts werden in drei Phasen simuliert:
\begin{enumerate}
......@@ -117,6 +119,52 @@ State Charts werden in drei Phasen simuliert:
\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. \\
......
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