next up previous contents
Nächste Seite: Das Needham-Schroeder Protokoll Aufwärts: Ein APA für das Needham-Schroeder Protokoll Vorherige Seite: Ein APA für das Needham-Schroeder Protokoll   Inhalt

formale Definition eines APA

Ein APA kann als eine Menge elementarer Automaten betrachtet werden. Der Zustand eines APA ist in einzelne Zustandskomponenten untergliedert. Die Zustandsmenge eines APA ergibt sich dann aus dem Kreuzprodukt der zu den einzelnen Komponenten gehörenden Zustandsmengen. Die Zustandsmengen der elementaren Automaten sind dann Teilmenge des Kreuzprodukts einiger Zustandskomponenten des APA (bzw. der dazugehörigen Zustandsmengen). Die elementaren Automaten haben gewissermaßen Zugriff auf einige der Zustandskomponenten und können miteinander kommunizieren, indem sie den Inhalt ihrer gemeinsamen Komponenten verändern.

Formal besteht ein APA $\mathcal(A)$ aus einer Familie von Zustandsmengen $(Z_S)$ (das entspricht den Zustandskomponenten), einer Familie elementarer Automaten $(A_e)$ einer Nachbarschaftsrelation $N$ und einem Startzustand $z_0$.

\begin{eqnarray*}
\mathcal(A) & = & [(Z_s)_{s \in \mathcal{S}}, (A_e)_{e \in \m...
...Phi_e \times T_e \\
z_0 & \in & \times_{S \in \mathcal(S)} Z_S
\end{eqnarray*}

$\mathcal{S}$ und $\mathcal{E}$ sind hierbei die Indexmengen für die Zustandsmengen bzw. die elementaren Automaten und $\mathcal{P}(\mathcal{S})$ entspricht der Potenzmenge von $\mathcal{S}$. Ein elementarer Automat ist ein Tupel aus einem Alphabet $\Phi_e$, einer Zustandsmenge $T_e$ und einer Zustandsüberführungsfunktion $\Delta_e$. Die Zustandsmenge $T_e$ eines elementaren Automaten ist dabei Teilmenge der Kreuzmenge aller benachbarten Zustandsmengen $Z_S, S\in N(e)$. Somit sind die elementaren Automaten über die Zustandskomponenten $Z_S$ entsprechend der Nachbarschaftsrelation miteinander verbunden. Weiterhin wird festgelegt, daß jeder elementare Automat mindestens eine benachbarte Zustandskomponente hat und jede Zustandskomponente mit mindestens einem elementaren Automaten verbunden sein muss:

\begin{eqnarray*}
& & \forall_{e \in \mathcal{E}}: N(e) \neq \emptyset \\
& & \mathcal{S} = \bigcup_{e \in \mathcal{E}} N(e)
\end{eqnarray*}

Ein Zustandsübergang im APA entspricht einem Zustandsübergang eines der enthaltenen elementaren Automaten. Das Verhalten eines APA wird daher durch alle möglichen Folgen von solchen Zustandsübergängen repräsentiert.


next up previous contents
Nächste Seite: Das Needham-Schroeder Protokoll Aufwärts: Ein APA für das Needham-Schroeder Protokoll Vorherige Seite: Ein APA für das Needham-Schroeder Protokoll   Inhalt
Michael Ueckerdt 2003-02-02