petrinetze.tex

\documentclass{cheat-sheet}

\pdfinfo{
  /Title (Zusammenfassung Petrinetze)
  /Author (Tim Baumann)
}

\usepackage{algorithmicx}
\usepackage[noend]{algpseudocode}
\usepackage{tikz}
\tikzset{
  font={\fontsize{6pt}{12}\selectfont}
}

\newcommand{\transition}{\square} % Transition
\newcommand{\place}{\bigcirc} % Stelle, Platz
\newcommand{\preset}[1]{{}^\bullet{#1}} % Vorbereich
\newcommand{\postset}[1]{{#1}^\bullet} % Nachbereich
\newcommand{\activeTransition}[1]{[{#1}\rangle} % aktive Transition
\newcommand{\labelledTransition}[1]{[{#1}\rangle\rangle} % beschriftete, aktive Transition
\DeclareMathOperator{\FS}{FS} % Menge der Schaltfolgen (firing sequences)
\newcommand{\ReachabilityGraph}{\mathfrak{R}} % Erreichbarkeitsgraph
\newcommand{\StepReachabilityGraph}{\mathfrak{SR}} % Schritt-Erreichbarkeitsgraph
\DeclareMathOperator{\Parikh}{Parikh} % Parikh-Bild
\newcommand{\inferrule}[2]{\frac{{#1}}{{#2}}} % logische Inferenzregel
\newcommand{\Markings}{\mathfrak{M}} % Menge von Markierungen
\newcommand{\ExtMarkings}{\mathfrak{M}^\omega} % Menge von erweiterten Markierungen
\DeclareMathOperator{\Fin}{Fin} % Menge von Endzuständen
\newcommand{\Lang}{\mathfrak{L}} % Sprachen von beschrifteten Netzen mit Endmarkierung
\newcommand{\fin}{\mathrm{fin}} % endlich
\newcommand{\Multisets}{\mathfrak{M}} % Multimengen
\DeclareMathOperator{\StepSequences}{SS} % Schrittfolgen
\newcommand{\SInv}{S\text{-}\mathrm{Inv}} % S-Invarianten
\newcommand{\TInv}{T\text{-}\mathrm{Inv}} % T-Invarianten
\newcommand{\reducesTo}{\mapsto} % reduziert zu (entscheidungsprobleme)
\newcommand{\reducesManyOneToLin}{\xmapsto{\mathrm{lin}}_M} % reduziert zu ... in linearer Zeit (entscheidungsprobleme)
\newcommand{\reducesManyOneToPoly}{\xmapsto{\mathrm{poly}}_M} % reduziert zu ... in polynomieller Zeit (entscheidungsprobleme)
\DeclareMathOperator{\Cov}{Cov} % Überdeckungsgraph
\newcommand{\nil}{\mathbf{nil}} % NULL
\DeclareMathOperator{\trans}{trans} % Transitionsabbildung
\DeclareMathOperator{\resTime}{res} % Restzeit, residual time
\DeclareMathOperator{\ready}{ready} % ready-Semantik
\newcommand{\Failure}{\mathfrak{F}} % Failure-Semantik
\newcommand{\parallelComposition}{\parallel} % Parallel-Komposition
\newcommand{\Powerset}{\mathcal{P}} % Potenzmenge

% Kleinere Klammern
\delimiterfactor=701

\setlength{\tabcolsep}{2pt}

\begin{document}

\raggedcolumns % stretche Inhalt nicht über die gesamte Spaltenhöhe

\maketitle{Zusammenfassung Petrinetze}

Dies ist eine Zusammenfassung zur gleichnamigen Vorlesung von Professor Dr. Walter Vogler im Wintersemester 2016/17.

% §2. Grundbegriffe

% 2.1
\begin{defn}
  Ein \emph{Netzgraph} ist ein Tripel $(S, T, W)$, wobei~$S$ und~$T$ disjunkte, endliche Mengen sind und $W : S \times T \cup T \times S \to \N$.
  Dadurch ist ein gerichteter, gewichteter, bipartiter Graph mit Kantenmenge $F = \Set{(x, y)}{W(x, y) \neq 0}$ gegeben.
\end{defn}

\begin{center}
  \begin{tabular}{r l l}
    Notation & Bezeichnung & Symbol \\ \hline
    $t \in T$ & \emph{Transition} & $\transition$ \\
    $s \in S$ & \emph{Stelle}, \emph{Platz} & $\place$ \\
    $(x, y) \in F$ & \emph{Kante} & $\xrightarrow{\enspace}$ falls $W(x, y) = 1$ \\
    && $\xrightarrow{w}$ falls $w \coloneqq W(x, y) > 1$
  \end{tabular}
\end{center}

\begin{defn}
  Sei $x \in S \cup T$.
  \begin{itemize}
    \item $\preset{x} \coloneqq \Set{y}{(y, x) \in F}$ heißt \emph{Vorbereich} von~$x$ und
    \item $\postset{x} \coloneqq \Set{y}{(x, y) \in F}$ heißt \emph{Nachbereich} von~$x$.
    \item $x$ heißt \emph{isoliert}, falls $\preset{x} \cup \postset{x} = \emptyset$.
    \item $x$ heißt \emph{vorwärts-verzweigt}, falls $\card{\postset{x}} \geq 2$ 
    \item $x$ heißt \emph{rückwärts-verzweigt}, falls $\card{\preset{x}} \geq 2$ 
  \end{itemize}
\end{defn}

\begin{defn}
  $(s, t) \in S \times T$ bilden eine \emph{Schlinge} falls $\{ (s, t), (t, s) \} \subseteq F$
\end{defn}

\begin{defn}
  Eine \emph{Markierung} ist eine Abbildung $M : S \to \N$. \\
  Eine Teilmenge $S' \subseteq S$ heißt \emph{markiert} unter~$M$, falls $\ex{s \in S'} M(s') > 0$, andernfalls \textit{unmarkiert}. \\
  Ein Element $s \in S$ heißt \textit{(un-)markiert}, falls $\{ s \} \subseteq S$ es ist.
\end{defn}

\begin{nota}
  $\Markings(S) \coloneqq \{ M : S \to \N \}$
\end{nota}

\begin{defn}
  Ein \emph{Petrinetz} $N = (S, T, W, M_N)$ besteht aus
  \begin{itemize}
    \item einem Netzgraphen $(S, T, W)$ und
    \item einer \textit{Anfangsmarkierung}~$M_N : S \to \N$.
  \end{itemize}
\end{defn}

\begin{nota}
  Für eine feste Transition $t \in T$ ist
  \[
    t^{-} : S \to \N, \enspace s \mapsto W(s, t), \qquad
    t^{+} : S \to \N, \enspace s \mapsto W(t, s)
  \]
\end{nota}

% 2.2
\begin{defn}
  Eine Transition $t \in T$ heißt \emph{aktiviert} unter einer Markierung~$M$, notiert $M \activeTransition{t}$, falls
  \[
    \fa{s \in S} W(s, t) \leq M(s) \iff
    t^{-} \leq M.
  \]
  Ist~$t$ aktiviert, so kann~$t$ \textit{schalten} und es entsteht die \textit{Folgemarkierung} $M' \coloneqq M + \Delta t$, wobei
  \[
    \Delta t : S \to \Z, \enspace s \mapsto W(t, s) - W(s, t).
  \]
\end{defn}

\begin{nota}
  $M \activeTransition{t} M'$
\end{nota}

\begin{defn}
  Für $w = t_1 \cdots t_n \in T^{*}$ und Markierungen~$M$ und~$M'$ gilt
  \[ M \activeTransition{w} M' \coloniff M \activeTransition{t_1} M_1 \activeTransition{t_2} \cdots \activeTransition{t_{n-1}} M_{n-1} \activeTransition{t_n} M' \]
  für (eindeutig bestimmte) Markierungen $M_1, \ldots, M_{n-1}$. \\
\end{defn}

\begin{defn}
  Ein Wort $w \in T^{*}$ heißt \emph{Schaltfolge} (\textit{firing sequence}) von~$N$, notiert $M_N \activeTransition{w}$, falls $\ex{M'} M_N \activeTransition{w} M'$.
\end{defn}

\begin{nota}
  \begin{minipage}[t]{0.8 \linewidth}
    $\activeTransition{M} \coloneqq \Set{M'}{\ex{w \in T^{*}} M \activeTransition{w} M'}$ \\
    $\FS(N) \coloneqq \Set{w \in T^{*}}{M_N \activeTransition{w}}$ \enspace
    für ein Petrinetz~$N$
  \end{minipage}
\end{nota}

\begin{defn}
  $M'$ heißt \emph{erreichbar} von~$M$, falls $M' \in \activeTransition{M}$.
\end{defn}

\begin{defn}
  $w \in T^\omega$ heißt \emph{unendliche Schaltfolge} von~$N$, falls alle endlichen Präfixe von~$w$ Schaltfolgen von~$N$ sind.
\end{defn}

\begin{defn}
  Eine Schaltfolge ist \emph{maximal}, falls sie endlich ist und in einer toten Markierung endet \textit{oder} unendlich ist. \\
  Eine Schaltfolge ist \emph{schwach/stark fair} für eine Trans.~$t \in T$ falls
  \begin{itemize}
    \item sie endlich ist und in einer Markierung endet, die~$t$ nicht aktiviert
    \item \textit{oder} $t$ unendlich ist und $t$ unendlich oft deaktiviert ist / $t$ nur endlich oft aktiviert ist
    \item \textit{oder} $t$ unendlich oft enthält.
  \end{itemize}
  Die Schaltfolge heißt \textit{schwach/stark fair}, falls sie für jede Transition schwach/stark fair ist.
\end{defn}

\begin{bem}
  stark fair $\implies$ schwach fair $\implies$ maximal
\end{bem}

\begin{defn}
  Der \emph{Erreichbarkeitsgraph} $\ReachabilityGraph(N)$ zu~$N$ besitzt die Knoten~$\activeTransition{M_N}$ und die Kanten $\Set{(M, M')}{\ex{t} M \activeTransition{t} M'}$.
\end{defn}

% 2.5
\begin{defn}
  $\Parikh : A^{*} \to \N^A, \enspace \Parikh(w)(a) \coloneqq \card{\Set{i}{w_i = a}}$
\end{defn}

% 2.6
\begin{lem}
  In $M \activeTransition{w} M'$ hängt~$M'$ nur von~$M$ und $\Parikh(w)$ ab, genauer
  \[
    M' = M + {\sum}_{t \in T} \Parikh(w)(t) \cdot \Delta t.
  \]
\end{lem}

% 2.7
\begin{lem}
  $M_1 \activeTransition{w} M_2 \implies M + M_1 \activeTransition{w} M + M_2$
\end{lem}

% ausgelassen: Satz 2.8, da trivial

% 2.10
\begin{lem}
  Sei $N$ ein Petri-Netz.
  Dann gilt:
  \begin{itemize}
    \item $\FS(N)$ ist \textit{präfix-abg.}, \dh{} $w = v u \in \FS(N) \implies v \in \FS(N)$.
    \item Ist $\activeTransition{M_N}$ endlich, so ist $\FS(N)$ regulär.
  \end{itemize}
\end{lem}

% 2.11
\begin{defn}
  Ein \emph{beschriftetes Petrinetz} $N = (S, T, W, M_N, \ell)$ best. aus
  \begin{itemize}
    \item einem Petrinetz $(S, T, W, M_N)$ und
    \item einer Transitionsbeschriftung (\textit{labelling}) $\ell : T \to \Sigma \cup \{ \lambda \}$, wobei~$\Sigma$ eine Menge von \textit{Aktionen} ist.
  \end{itemize}
\end{defn}

\begin{sprechweise}
  $t \in T$ mit $\ell(t) = \lambda$ heißt \textit{intern} oder \textit{unsichtbar}.
\end{sprechweise}

\begin{nota}
  \begin{minipage}[t]{0.8 \linewidth}
    Für $t \in T^{*}$ ist $\ell(w) \coloneqq \ell(t_1) \cdots \ell(t_n) \in \Sigma^{*}$. \\
    Dabei wird $\lambda$ als das leere Wort in $\Sigma^{*}$ aufgefasst.
  \end{minipage}
\end{nota}

\begin{defn}
  Mit $t \in T$, $w \in T^{*}$ und Markierungen $M$, $M'$ ist definiert:
  \[
    \inferrule
      {M \activeTransition{t} M'}
      {M \labelledTransition{\ell(t)} M'} \quad
    \inferrule
      {M \activeTransition{t}}
      {M \labelledTransition{\ell(t)}} \quad
    \inferrule
      {M \activeTransition{w} M'}
      {M \labelledTransition{\ell(w)} M'} \quad
    \inferrule
      {M \activeTransition{w}}
      {M \labelledTransition{\ell(w)}}
  \]
\end{defn}

\begin{defn}
  Die \emph{Sprache} eines beschrift. Netzes~$N$ ist
  \[
    L(N) \coloneqq \Set{v \in \Sigma^{*}}{M_n \labelledTransition{v}}.
  \]
\end{defn}

% 2.12
\begin{defn}
  Ein \emph{beschriftetes Netz mit Endmarkierung} ist ein Tupel $N = (S, T, W, M_N, \ell, \Fin)$ wobei
  $(S, T, W, M_N, \ell)$ ein beschriftetes Netz und
  $\Fin \subseteq \Markings(S)$ eine endl. Menge von \textit{Endmarkierungen} ist.
  Die entspr. Sprache ist $L_\fin(N) \coloneqq \Set{v \in \Sigma^{*}}{\ex{M \in \Fin} M_N \activeTransition{v} M}$.
\end{defn}

\begin{nota}
  $\Lang^\lambda \coloneqq \Set{L_\fin(N)}{N \text{ beschrift. Netz mit Endmarkierung}}$ \\
  $\Lang \coloneqq \Set{L_\fin(N)}{N \text{ beschrift. Netz mit Endmark. ohne interne Trans.}}$
\end{nota}

% 2.13
\begin{satz}
  $\{ \text{ reguläre Sprachen } \} \subseteq \Lang$
\end{satz}

\subsection{Nebenläufigkeit I}

% 2.14
\begin{defn}
  Eine Multimenge über~$X$ ist eine Funktion $\mu : X \to \N$.
\end{defn}

\begin{nota}
  \begin{minipage}[t]{0.8 \linewidth}
    $\Multisets(X) \coloneqq \{ \mu : X \to \N \}$ \\
    $\mu_Y \in \Multisets(X), \, \mu_Y(x) \coloneqq \card{\Set{\star}{x \in Y}}$ für $Y \subset X$, \\
    $\emptyset \coloneqq \mu_\emptyset \in \Multisets(X)$, \enspace
    $\mu_x \coloneqq \mu_{\{ x \}} \in \Multisets(X)$ für $x \in X$
  \end{minipage}
\end{nota}

% 2.15
\begin{defn}
  Ein \emph{Schritt}~$\mu$ ist eine Multimenge $\mu \neq \emptyset \in \Multisets(T)$. \\
  Der Schritt~$\mu$ ist \emph{aktiviert} unter~$M$, notiert $M \activeTransition{\mu}$, falls
  \[
    \fa{s \in S} \mu^{-}(s) \coloneqq {\sum}_{t \in T} \mu(t) W(s, t) \leq M(s).
  \]
  Durch \textit{Schalten} von~$\mu$ entsteht die Folgemarkierung $M' \in \Markings(S)$ mit
  \[
    M'(s) = M(s) + {\sum}_{t \in T} \mu(t) \cdot (W(t, s) - W(s, t)).
  \]
\end{defn}

\begin{bem}
  \begin{minipage}[t]{0.8 \linewidth}
    Analog wird verallgemeinert:
    $M \activeTransition{\mu} M'$, $M \activeTransition{w}$, $M \activeTransition{w} M'$ \\
    für $\mu \in \Markings(T) \setminus \{ \emptyset \}$ bzw. $w \in (\Markings(T) \setminus \{ \emptyset \})^{*}$.
  \end{minipage}
\end{bem}

\begin{defn}
  \begin{minipage}[t]{0.8 \linewidth}
    $\StepSequences(N) \coloneqq \Set{w \in (\Markings(T) \setminus \{ \emptyset \})^{*}}{M_N \activeTransition{w}}$ \\
    heißen \emph{Schrittfolgen} (\textit{step sequences}).
  \end{minipage}
\end{defn}

\begin{defn}
  Zwei Transitionen $t, t' \in T$ mit $M \activeTransition{t}$ und $M \activeTransition{t'}$ sind
  \begin{itemize}
    \item \emph{nebenläufig} \textit{unter~$M$}, falls $M \activeTransition{t + t'}$,
    \item \emph{in Konflikt} \textit{unter~$M$}, falls $\neg M \activeTransition{t + t'}$.
  \end{itemize}
\end{defn}

\begin{nota}
  Für $\mu \in \Multisets(T)$ ist $\ell(\mu)$ die Multimenge mit
  \[
    \ell(\mu) : \Sigma \to \N, \enspace
    x \mapsto {\sum}_{t \in T, \ell(t) = x} \mu(t)
  \]
  (falls die rechte Zahl endlich ist für alle $x \in \Sigma$). \\
  Für $w = \mu_1 \cdots \mu_n \in \Multisets(T)^{*}$ ist 
  $\ell(w) \coloneqq \ell(\mu_1) \cdots \ell(\mu_n)$.
\end{nota}

\begin{defn}
  Mit $\mu \in \Markings(T) \setminus \{ 0 \}$, $w \in (\Markings(T) \setminus \{ 0 \})^{*}$ und $M$, $M'$ ist defin.:
  \[
    \inferrule
      {M \activeTransition{\mu} M'}
      {M \labelledTransition{\ell(\mu)} M'} \quad
    \inferrule
      {M \activeTransition{\mu}}
      {M \labelledTransition{\ell(\mu)}} \quad
    \inferrule
      {M \activeTransition{w} M'}
      {M \labelledTransition{\ell(w)} M'} \quad
    \inferrule
      {M \activeTransition{w}}
      {M \labelledTransition{\ell(w)}}
  \]
\end{defn}

% 2.16
\begin{lem}
  $M \activeTransition{t_1}, \ldots, M \activeTransition{t_n} \wedge \fa{i \neq j} \preset{t_i} \cap \preset{t_j} = \emptyset \implies M \activeTransition{t_1 + \ldots t_n}$
\end{lem}

% 2.17
\begin{lem}
  $M \activeTransition{\mu} M' \wedge \Parikh(w) = \mu \implies M \activeTransition{w} M'$
\end{lem}

\begin{bem}
  Über Schrittfolgen werden somit dieselben Markierungen erreicht wie über Schaltfolgen.
\end{bem}

\begin{defn}
  Der \emph{schrittweise Erreichbarkeitsgraph}~$\StepReachabilityGraph(N)$ besitzt die Knoten $\activeTransition{M}$ und die Kanten $\Set{(M, M')}{\ex{\mu \in \Markings(T) \!\setminus\! \{ \emptyset \}} M \activeTransition{\mu} M'}$.
\end{defn}

% 2.18
\begin{lem}
  Sei~$N$ schlingenfrei. Dann gilt:
  \[
    (\fa{w \in T^{*}, \Parikh(w) = \mu} M \activeTransition{w}) \iff M \activeTransition{\mu}
  \]
\end{lem}

% Erreichbarkeit

% (Problemdefinitionen nach hinten verschoben)

% 2.19
\begin{defn}
  Eine Stelle $s \in S$ heißt \emph{$n$-beschränkt} / \emph{beschränkt}, falls
  \[
    \sup \Set{M(s)}{M \in \activeTransition{M_N}} \leq n
    \quad / \quad
    \sup \Set{M(s)}{M \in \activeTransition{M_N}} < \infty.
  \]
  Ein Netz heißt ($n$-) \textit{beschränkt}, wenn alle Stellen $s \in S$ ($n$-) beschränkt sind.
  Ein Netz heißt \emph{sicher}, wenn es 1-beschränkt ist. \\
  % Def 3.6:
  Ein Netz heißt \emph{strukturell beschränkt}, wenn es bei beliebig geänderter Anfangsmarkierung beschränkt ist.
\end{defn}

% 2.20
\begin{prop}
  $\activeTransition{M_N}$ endlich $\iff$ $N$ beschränkt
\end{prop}

% Verklemmung

\section{Lebendigkeit}

% 2.21
\begin{defn}
  Sei $t \in T$ eine Trans. in einem Netz~$N$ und~$M$ eine Markierung.
  \begin{itemize}
    \item $t$ heißt \emph{tot} (oder \textit{0-lebendig}) \textit{unter~$M$}, falls $\fa{M' \in \activeTransition{M}} \neg M' \activeTransition{t}$.
    \item $t$ heißt \textit{1-lebendig unter~$M$}, falls $\ex{w \in T^*} M \activeTransition{w t}$
    \item $t$ heißt \textit{2-lebendig unter~$M$}, falls
    \[ \fa{n \in \N} \ex{w_1, \ldots, w_n \in T^*} M \activeTransition{w_1 t w_2 t \cdots w_n t} \]
    \item $t$ heißt \textit{3-lebendig unter~$M$}, falls eine unendliche Schaltfolge~$w$ existiert, $M \activeTransition{w}$, die~$t$ unendlich oft enthält.
    \item $t$ heißt \emph{(4-)\,lebendig} \textit{unter $M$}, falls
    \[ \fa{M' \in \activeTransition{M}} \neg (t \text{ ist tot unter~$M$}) \]
    \item $t$ heißt \textit{lebendig}, falls $t$ lebendig unter~$M_N$ ist.
  \end{itemize}
\end{defn}

\begin{bem}
  \begin{minipage}[t]{0.8 \linewidth}
    $t$ 4-lebendig $\implies$ $t$ 3-lebendig $\implies$ $t$ 2-lebendig $\implies$ \\
    $t$ 1-lebendig $\iff$ $\neg$ ($t$ 0-lebendig)
  \end{minipage}
\end{bem}

\begin{defn}
  Bezogen auf eine Markierung~$M$:
  \begin{itemize}
    \item $M$ heißt \textit{tot}, falls alle Transitionen unter~$M$ tot sind.
    \item $M$ heißt \textit{lebendig}, wenn alle $t \in T$ unter~$M$ lebendig sind.
    \item $M$ heißt \emph{monoton lebendig}, wenn alle $M' \geq M$ lebendig sind.
  \end{itemize}
\end{defn}

\begin{bem}
  $M \text{ ist tot} \iff \fa{t \in T} \neg M \activeTransition{t}$
\end{bem}

\begin{defn}
  Bezogen auf ein Netz~$N$:
  \begin{itemize}
    \item $N$ heißt \textit{tot}, falls $M_N$ tot ist.
    \item $N$ heißt \emph{verklemmungsfrei}, falls $\fa{M \in \activeTransition{M_N}} \neg (M \text{ tot})$
    \item $N$ heißt \textit{lebendig}, wenn $M_N$ lebendig ist.
    \item $N$ heißt \textit{monoton lebendig}, wenn $M_N$ monoton lebendig ist.
  \end{itemize}
\end{defn}

% §3. S- und T-Invarianten
\section{$S$- und $T$-Invarianten}

% Ausgelassen: Beispiel mit 3 lesenden, zwei schreibenden Prozessen

% 3.1
\begin{defn}
  Die \emph{Inzidenzmatrix} \textit{eines Netzes~$N$} ist die Matrix $C(N) \in \Z^{T \times S}$ mit $C(N)_{s t} = \Delta t (s)$ für $s \in S$ und $t \in T$.
\end{defn}

\begin{bem}
  Folglich ist $\Delta t = C(N) \cdot t$ (wenn man $t$ als One-Hot-Vektor auffasst) und für $M \activeTransition{w} M'$ ist $M' = M + C(N) \cdot \Parikh(w)$.
\end{bem}

% 3.2
\begin{defn}
  Eine \emph{$S$-Invariante} $y : S \to \Z$ ist eine Lsg von $C(N)^T \cdot y = 0$. \\
  Der \emph{Träger} $\supp(y)$ \textit{einer $S$-Invarianten~$y$} ist $\Set{s \in S}{y(s) \neq 0}$. \\
\end{defn}

\begin{nota}
  $\SInv(N) \coloneqq \{ \text{ $S$-Invarianten von~$N$ } \} = \ker(C(N)^T)$
\end{nota}

\begin{lemdefn}
  Das Netz~$N$ heißt \emph{von $S$-Invarianten überdeckt}, falls folgende äquivalente Bedingungen gelten:
  \begin{itemize}
    \item $N$ besitzt eine positive (\dh{} $\fa{s \in S} y(s) > 0$) $S$-Invariante.
    \item Für alle $s \in S$ gibt es eine nichtnegative (\dh{} $\fa{s \in S} y(s) \geq 0$) $S$-Invariante mit $s \in \supp(y)$.
  \end{itemize}
\end{lemdefn}

% 3.3 + 3.4
\begin{lem}
  Für $y \in \Z^S$ gilt
  \[
    y \in \SInv(N) \implies \fa{M \in \activeTransition{M_N}} y^T \cdot M = y^T \cdot M_N.
  \]
  Ist jede Transition in~$N$ 1-lebendig, so gilt auch die Rückrichtung:
  \[
    y \in \SInv(N) \iff \fa{M \in \activeTransition{M_N}} y^T \cdot M = y^T \cdot M_N
  \]
\end{lem}

\begin{bem}
  Das Lemma kann verwendet werden um zu zeigen, dass eine Markierung~$M$ nicht erreichbar ist.
\end{bem}

% 3.5
\begin{lem}
  Sei $s \in S$ und $y \in \SInv(N)$ nichtnegativ mit $y(s) > 0$. \\
  Dann ist $s$ beschränkt, genauer $(y^T \cdot M_N / y(s))$-beschränkt.
\end{lem}

% 3.6
\begin{satz}
  Ist~$N$ von $S$-Invarianten überdeckt, so ist~$N$ strukturell beschränkt.
  % Satz 11.10 in "Analyse von Petri-Netz-Modellen" von Peter H. Starke
  Besitzt $N$ eine lebendige Markierung, so gilt sogar:
  \[
    \text{$N$ ist strukturell beschr.} \iff
    \text{$N$ ist von $S$-Invarianten überdeckt.}
  \]
\end{satz}

\begin{defn}
  Ein \emph{home state} ist eine Markierung~$M$ mit
  \[
    \fa{M' \in \activeTransition{M}} M \in \activeTransition{M'}.
  \]
  Ein Netz~$N$ heißt \emph{reversibel}, wenn $M_N$ ein home state ist.
\end{defn}

\begin{lem}
  Angenommen, $N$ ist reversibel und keine Transitionen sind tot unter~$M_N$.
  Dann ist $N$ lebendig.
\end{lem}

\begin{bem}
  Es gibt lebendige, sichere Netze, die \textit{nicht} von $S$-Invarianten überdeckt sind.
\end{bem}

% 3.8
\begin{defn}
  Eine \emph{$T$-Invariante} $x : T \to \Z$ ist eine Lsg von $C(N) \cdot x = 0$.
  Das Netz~$N$ heißt \emph{von $T$-Invarianten überdeckt}, wenn es eine positive $T$-Invariante gibt.
\end{defn}

\begin{nota}
  $\TInv(N) \coloneqq \{ \text{ $T$-Invarianten von~$N$ } \} = \ker(C(N))$
\end{nota}

% 3.9
\begin{lem}
  Sei $w \in T^*$ mit $M \activeTransition{w} M'$.
  Dann gilt:
  \[
    \Parikh(w) \in \TInv(N) \iff M = M'
  \]
\end{lem}

\begin{satz}
  Ist~$N$ lebendig und beschränkt, so ist $N$ von $T$-Invarianten überdeckt.
\end{satz}

\section{State Transition Graphs}

\begin{defn}
  Ein \emph{State Transition Graph} (STG) mit \textit{Eingangssignal- menge}~$I$ und \textit{Ausgangssignalmenge}~$O$ ist ein sicheres Petri-Netz~$N$, dessen Transitionen mit \textit{Signalflanken} $a{+}$ oder $a{-}$ mit $a \in A \coloneqq I \cup O$ beschriftet sind, \dh{}
  \[ \Sigma = \Set{a{+}}{a \in A} \cup \Set{a{-}}{a \in A}. \]
\end{defn}

\begin{defn}
  Der STG~$N$ heißt \emph{konsistent}, falls es für jede erreichbare Markierung $M \in \activeTransition{M_N}$ einen Code $C(M) \in \{ 0, 1 \}^A$ gibt, sodass
  \begin{itemize}
    \item $C(M_N)(a) = 0$
    \item $M \labelledTransition{a{+}} M' \implies C(M)(a) = 0 \wedge C(M')(a) = 1$
    \item $M \labelledTransition{a{-}} M' \implies C(M)(a) = 1 \wedge C(M')(a) = 0$
  \end{itemize}
  für alle Markierungen $M, M' \in \activeTransition{M_N}$ und Signale $a \in A$.
\end{defn}

\begin{bem}
  Der Code ist (im Falle der Existenz) eindeutig bestimmt durch
  \[
    C(M)(a) \coloneqq \card{\Set{i}{w_i = a{+}}} - \card{\Set{i}{w_i = a{-}}}
  \]
  für ein $w \in \Sigma^*$ mit $M_N \labelledTransition{w} M$.
\end{bem}

\begin{beob}
  Ist der STG $N$ konsistent, so gibt es
  \begin{enumerate}
    \item kein $w = u \, a{+} \, v \, a{+} \in \Sigma^*$ mit $u \in \Sigma^*$ und $v \in (\Sigma \setminus \{ a{-} \})$,
    \item kein $w = u \, a{-} \, v \, a{-} \in \Sigma^*$ mit $u \in \Sigma^*$ und $v \in (\Sigma \setminus \{ a{+} \})$ und
    \item kein $w = u \, a{-} \in \Sigma^*$ mit $u \in (\Sigma \setminus \{ a{+} \})^*$
  \end{enumerate}
  sodass jeweils $M_N \labelledTransition{w}$ gilt.
\end{beob}

\begin{defn}
  Der STG~$N$ \emph{hat CSC} (\textit{Complete State Coding}), falls für alle $M, M' \in \activeTransition{M_N}$ mit $C(M) = C(M')$ und \textit{Ausgabesignale} $a \in O$ gilt:
  \[
    M \activeTransition{a {+}} \iff M' \activeTransition{a {+}}
    \quad \text{bzw.} \quad
    M \activeTransition{a {-}} \iff M' \activeTransition{a {-}}.
  \]
  Ansonsten hat~$N$ einen \textit{CSC-Konflikt}.
\end{defn}

\begin{defn}
  Der STG hat einen \emph{IO-Konflikt}, falls eine Markierung $M \in \activeTransition{M_N}$ und Transitionen $t_i \in \Sigma_I \coloneqq \Set{a{+}}{a \in I} \cup \Set{a{-}}{a \in I}$ sowie $t_o \in \Sigma_O \coloneqq \Set{b{+}}{b \in O} \cup \Set{b{-}}{b \in O}$ existieren, sodass $t_i$ und $t_o$ unter~$M$ in Konflikt stehen, \dh{}
  \[
    M \activeTransition{t_i}
    \enspace \text{und} \enspace
    M \activeTransition{t_o}
    \enspace \text{aber} \enspace
    \neg (M \activeTransition{t_i + t_o}).
  \]
\end{defn}


% §4. Einige Entscheidbarkeitsprobleme

\section{Einige Entscheidbarkeitsprobleme}

\begin{probleme}
  Gegeben sei eine Netz~$N$
  \begin{itemize}
    \item \emph{Erreichbarkeit} (E):
      \ldots und eine Markierung~$M$.
      Frage: Ist~$M$ erreichbar in~$N$, gilt also $M \in \activeTransition{M_N}$?
    \item \emph{$0$-Erreichbarkeit} (O-E):
      Frage: Ist $0 \in \activeTransition{M_N}$?
    \item \emph{Teilerreichbarkeit} (TE):
      \ldots eine Teilmenge $S' \subseteq S$ und $M : S' \to \N$.
      Frage: Gibt es ein $M \in \activeTransition{M_N}$ mit $M|_{S'} = M'$?
  \end{itemize}
\end{probleme}

\begin{bem}
  Diese Probleme sind lösbar, falls der Erreichbarkeitsgraph endlich ist.
\end{bem}

% ausgelassen: Definition 4.1 von Entscheidungsproblem und Entscheidungsverfahren

\begin{defn}
  \begin{itemize}
    \item Ein Entscheidungsproblem~$A$ ist auf ein Entscheidungs- problem~$B$ \emph{reduzierbar} (notiert $A \reducesTo B$), falls ein Lösungsalgo- rithmus für~$A$ existiert, welcher einen (vllt. gar nicht existenten!) Lösungsalgorithmus für~$B$ verwenden darf.
    \item $A$ ist \emph{linear / polynomiell many-one-reduzierbar} \textit{auf~$B$}, falls aus einer Instanz~$I$ von~$A$ in linearer / polynomieller Zeit eine Instanz~$I'$ von~$B$ berechnet werden kann, sodass die Antwort auf~$I$ gleich der Antwort auf~$I'$ ist. \\
    Notation: $A \reducesManyOneToLin B$ / $A \reducesManyOneToPoly B$
  \end{itemize}
\end{defn}

% 4.2
\begin{satz}
  $\text{(0-E)} \reducesManyOneToLin \text{(E)} \reducesManyOneToLin \text{(TE)}  \reducesManyOneToLin \text{(0-E)}$
\end{satz}

\begin{beweis}[$\text{(TE)}  \reducesManyOneToLin \text{(0-E)}$]
  Konstruiere $\overline{N} = (\overline{S}, \overline{T}, \overline{W}, M_{\overline{N}})$ mit
  \begin{align*}
    \overline{S} & \coloneqq S \amalg \Set{\overline{s'}}{s' \in S'} \\
    \overline{T} & \coloneqq T \amalg \Set{t_{s'}}{s' \in S'} \amalg \Set{t_s}{s \in S \setminus S'} \\
    \overline{W} & \coloneqq W \cup \Set{s \to t_s}{s \in S \setminus S'} \cup \Set{s' \to t_{s'} \leftarrow \overline{s'}}{s' \in S'} \\
    M_{\overline{N}} & \coloneqq (s \in S \mapsto M_N(s), \enspace \overline{s'} \mapsto M'(s'))
  \end{align*}
  Dann: $M'$ teilerreichbar in~$N$ $\iff$ Nullmark. erreichbar in~$\overline{N}$
  \begin{center}\begin{tikzpicture}
    \draw (0,-0.25) rectangle (8, 4.25);
    \node[anchor=west] at (0.15, 0.15) {$\text{(TE)}  \reducesManyOneToLin \text{(0-E)}$};
    \node at (0.75, 3.75) {\normalsize $N$};
    \draw (4, 3) ellipse (3.5 and 0.75);
    \node[circle,draw] (s1) at (1.5,3) {$s_1$};
    \node[draw] (ts1) at (1.5, 1.75) {$t_{s_1}$};
    \draw[->] (s1) -- (ts1);
    \node at (2.25, 3) {$\cdots$};
    \node at (2.25, 1.75) {$\cdots$};
    \node[circle,draw] (sn) at (3,3) {$s_n$};
    \node[draw] (tsn) at (3, 1.75) {$t_{s_n}$};
    \draw[->] (sn) -- (tsn);
    \node at (4, 3.5) {\normalsize $S'$};
    \draw (5.5, 3) ellipse (1.5 and 0.5);
    \node[circle,draw] (sp1) at (4.75,3) {$s'_1$};
    \node[draw] (tsp1) at (4.75, 1.75) {$t_{s'_1}$};
    \node[circle,draw] (sp1o) at (4.75, 0.5) {$\overline{s'_1}$};
    \draw[->] (sp1) -- (tsp1);
    \draw[->] (sp1o) -- (tsp1);
    \node at (5.5, 3) {$\cdots$};
    \node at (5.5, 1.75) {$\cdots$};
    \node at (5.5, 0.5) {$\cdots$};
    \node[circle,draw] (spm) at (6.25,3) {$s'_m$};
    \node[draw] (tspm) at (6.25, 1.75) {$t_{s'_m}$};
    \node[circle,draw] (spmo) at (6.25,0.5) {$\overline{s'_m}$};
    \draw[->] (spm) -- (tspm);
    \draw[->] (spmo) -- (tspm);
  \end{tikzpicture}\end{center}
\end{beweis}

% 4.3
\begin{satz}[schwierig!]
  (E) ist entscheidbar.
\end{satz}

\begin{probleme}
  Gegeben sei ein Petrinetz~$N$
  \begin{itemize}
    \item \emph{Lebendigkeit} (L): 
      Frage: Ist $N$ lebendig?
    \item \emph{Einzellebendigkeit} (EL):
      \ldots und $t \in T$.
      Frage: Ist $t$ lebendig?
  \end{itemize}
\end{probleme}

% ausgelassen: 4.4 da gleichzeitig 4.5

% 4.5
\begin{satz}
  $\text{(L)} \reducesManyOneToLin \text{(EL)} \reducesManyOneToLin \text{(L)}$
\end{satz}

\begin{beweis}
  "`$\text{(L)} \reducesManyOneToLin \text{(EL)}$"'.
  Konstruiere $\overline{N} = (\overline{S}, \overline{T}, \overline{W}, M_{\overline{N}})$ mit
  \begin{align*}
    \overline{S} & \coloneqq S \amalg \Set{s_t}{t \in T} \\
    \overline{T} & \coloneqq T \amalg \{ t_\mathrm{afterall} \} \\
    \overline{W} & \coloneqq W \cup \Set{t \to s_t}{t \in T} \cup \Set{s_t \to t_\mathrm{afterall}}{t \in T} \\
    M_{\overline{N}} & \coloneqq (s \in S \mapsto M_N(s), \enspace s_t \mapsto 0)
  \end{align*}
  Dann: $N$ lebendig $\iff$ $t_\mathrm{afterall}$ lebendig in $\overline{N}$.
  
  \begin{center}\begin{tikzpicture}
    \draw (0,0) rectangle (6, 3.5);
    \node[anchor=west] at (0.15, 0.4) {$\text{(L)}  \reducesManyOneToLin \text{(EL)}$};
    \node at (0.55, 3.15) {\normalsize $N$};
    \draw (1.25, 2) ellipse (0.75 and 1.25);
    \node[draw] (t1) at (1.25, 2.75) {$t_1$};
    \node at (1.25, 2.1) {$\vdots$};
    \node[draw] (tn) at (1.25, 1.25) {$t_n$};
    \node[draw,circle] (st1) at (3, 2.75) {$s_{t_1}$};
    \node at (3, 2.1) {$\vdots$};
    \node[draw,circle] (stn) at (3, 1.25) {$s_{t_n}$};
    \draw[->] (t1) -- (st1);
    \draw[->] (tn) -- (stn);
    \node[draw] (tafterall) at (5, 2) {$t_\mathrm{afterall}$};
    \draw[->] (st1) to [bend left=30] (tafterall);
    \draw[->] (stn) to [bend right=30] (tafterall);
  \end{tikzpicture}\end{center}

  "`$\text{(EL)} \reducesManyOneToLin \text{(L)}$"'.
  Beweisidee: 
  % siehe 5.1.4 in "Petri-Netze" von Priese und Wimmel
  Gefragt sei, ob eine Transition~$t_0$ in Netz~$N$ lebendig ist.
  Erweitere~$N$ zu einem Netz~$\hat{N}$, sodass jede Transition~$t$ aus~$N$ außer~$t_0$ und jede neue Transition lebendig ist (indem man die nötigen Marken zum Schalten von~$t$ bereitstellt und nach dem Schalten die durch~$t$ erzeugten Marken entfernt). \\
  Dann zeige: \enspace $\hat{N}$ lebendig $\iff$ $t_0$ lebendig in~$N$.
\end{beweis}

% 4.4 b)
\begin{satz}
  (EL) ist reduzierbar auf (TE)
\end{satz}

\begin{beweisidee}
  Setze
  \begin{align*}
    T_{t_0} & \coloneqq \Set{M \in \ExtMarkings(N)}{\text{$t_0$ tot in~$M$}} \\
    T_{t_0}^{\mathrm{max}} & \coloneqq \Set{M \in T_{t_0}}{\text{$M$ ist maximal in $T_{t_0}$}} \\
    S'(M) & \coloneqq \Set{s \in S}{M(s) < \infty} \enspace \text{für $M \in \ExtMarkings(N)$}
  \end{align*}
  Es gilt:
  \[
    \arraycolsep=1pt
    \begin{array}{l l}
      & t_0 \text{ ist nicht lebendig} \\
      \iff & \ex{M \in \activeTransition{M_N}} t \text{ tot in~$M$} \\
      \iff & \ex{M \in \activeTransition{M_N}} \ex{M^\omega \in T_{t_0}^{\mathrm{max}}} M \leq M^\omega \\
      \iff & \ex{M^\omega \in T_{t_0}^{\mathrm{max}}} \ex{M' \leq M^\omega|_{S'(M^\omega)}} M' \text{ teilerreichbar in } N
    \end{array}
  \]
  Nach dem Lemma von Dickson ist $T_{t_0}^{\mathrm{max}}$ endlich.
  Man kann zeigen, dass~$T_{t_0}^{\mathrm{max}}$ auch berechenbar ist.
  Somit ist die Bedingung der letzten Zeile algorithmisch nachprüfbar.
\end{beweisidee}

% 4.4 c), abgewandelt (Reduktion auf EL statt auf L, siehe Priese, Wimmel, "Petrinetze", Satz 5.1.5)
\begin{satz}
  (0-E) $\reducesManyOneToLin$ Co-(EL), das ist (EL) mit umgekehrter Antwort
\end{satz}

\begin{beweis}
  Konstruiere $\overline{N} = (\overline{S}, \overline{T}, \overline{W}, M_{\overline{N}})$ mit
  \begin{align*}
    \overline{S} & \coloneqq S \amalg \{ s_\text{s-ctrl}, s_\text{t-ctrl} \} \\
    \overline{T} & \coloneqq T \amalg \Set{t_s}{s \in S} \amalg \{ t_0 \} \\
    \overline{W} & \coloneqq W \cup \Set{t \rightleftarrows s_\text{t-ctrl}}{t \in T} \cup \Set{s \rightleftarrows t_s}{s \in S} \\
    & \cup \Set{s_\text{s-ctrl} \to t_s \to s_\text{t-ctrl}}{s \in S} \cup \{ s_\text{t-ctrl} \to t_0 \to s_\text{s-ctrl} \} \\
    M_{\overline{N}} & \coloneqq (s \in S \mapsto M_N(s), \enspace s_\text{s-ctrl} \mapsto 0, \enspace s_\text{t-ctrl} \mapsto 1)
  \end{align*}
  Dann: Nullmark. in $N$ erreichbar $\iff$ $t_0$ in $\overline{N}$ nicht lebendig

  \begin{center}\begin{tikzpicture}
    \draw (0,-0.25) rectangle (8, 4.25);
    \node[anchor=west] at (0.15, 0.15) {(0-E) $\reducesManyOneToLin$ Co-(EL)};
    \node at (0.75, 3.75) {\normalsize $N$};
    \draw (4, 3) ellipse (3.5 and 0.75);
    \node[circle,draw] (s1) at (1.5,3) {$s_1$};
    \node[circle,draw] (sn) at (3,3) {$s_n$};
    \node at (2.25, 3) {$\cdots$};
    \node[draw] (ts1) at (1.5, 1.75) {$t_{s_1}$};
    \node[draw] (tsn) at (3, 1.75) {$t_{s_n}$};
    \node at (2.25, 1.75) {$\cdots$};
    \node[circle,draw] (ssc) at (2.25, 0.5) {$\,\,$};
    \node[draw] (t1) at (5,3) {$t_1$};
    \node[draw] (tm) at (6.5,3) {$t_m$};
    \node at (5.75, 3) {$\cdots$};
    \node[circle,draw] (stc) at (5.75, 0.5) {$\bullet$};
    \node[draw] (t0) at (4, 0.5) {$t_0$};
    \draw[<->] (s1) -- (ts1);
    \draw[<->] (sn) -- (tsn);
    \draw[->] (ts1) to [bend left=3] (stc);
    \draw[->] (tsn) to [bend left=12] (stc);
    \draw[->] (ssc) to [bend left=20] (ts1);
    \draw[->] (ssc) to [bend right=20] (tsn);
    \draw[<->] (t1) to [bend right=10] (stc);
    \draw[<->] (tm) to [bend left=10] (stc);
    \draw[->] (stc) -- (t0);
    \draw[->] (t0) -- (ssc);
  \end{tikzpicture}\end{center}
\end{beweis}

\begin{problem}[\emph{Spezielles Reproduktionsproblem} (SR)]
  Gegeben ein Netz~$N$, gibt es eine nicht-leere Schaltfolge~$w$ mit $M_N \activeTransition{w} M_N$?
\end{problem}

% ÜB 8, Aufgabe 1
\begin{satz}
  $\text{(SR)} \reducesManyOneToLin \text{(0-E)}$
\end{satz}

\begin{beweis}
  Konstruiere $\widetilde{N} = (\widetilde{S}, \widetilde{T}, \widetilde{W}, M_{\widetilde{N}})$ mit
  \begin{align*}
    & \widetilde{S} \coloneqq S \times \{ \text{active}, \text{comparison} \} \amalg \{ s_{\mathrm{control}} \} \\
    & \widetilde{T} \coloneqq T \times \{ \text{one-shot}, \mathrm{multiple} \} \amalg \Set{t_s}{s \in S} \\
    & \widetilde{W}((t, \_\_), (s, \mathrm{active})) \coloneqq W(t, s), \qquad
    \widetilde{W}(s_\text{control}, (t, \text{one-shot})) \coloneqq 1, \\
    & \widetilde{W}((s, \text{active}), (t, \_\_)) \coloneqq W(s, t) \qquad
    \widetilde{W}((s, \_\_), t_s) \coloneqq 1, \\
    & \widetilde{W}(\_\_, \_\_) \coloneqq 0 \text{ sonst}, \quad
    M_{\widetilde{N}}(s, \_\_) \coloneqq M_N(s), \quad
    M_{\widetilde{N}}(s_\mathrm{control}) \coloneqq 1
  \end{align*}
  Dann gilt: \quad
  $\ex{w \in t^* \setminus \{\lambda\}} M_N \activeTransition{w} M_N \iff 0 \in \activeTransition{M_{\widetilde{N}}}$
\end{beweis}

\begin{fazit}
  Im folgenden Bild sind alle Reduktionen eingezeichnet.
  Dabei handelt es sich um lineare Many-One-Reduktionen mit Ausnahme von (EL) $\reducesTo$ (TE).

  \begin{center}\begin{tikzpicture}
    \node (SR) at (-1.5, 3) {(SR)};
    \node (NE) at (0,3) {(0-E)};
    \node (E) at (0,2) {(E)};
    \node (TE) at (0,1) {(TE)};
    \node (L) at (1.5,2.5) {(L)};
    \node (EL) at (1.5,1.5) {(EL)};
    \draw[|->] (SR) to (NE);
    \draw[|->] (NE) to (E);
    \draw[|->] (E) to (TE);
    \draw[|->] (TE) to [bend left=60] (NE);
    \draw[|->] (L) to [bend left=20] (EL);
    \draw[|->] (EL) to [bend left=20] (L);
    \draw[|->] (NE) to [bend right=5] (EL);
    \draw[|->] (EL) to [bend left=10] (TE);
  \end{tikzpicture}\end{center}

  (L) und (EL) sind entscheidbar, aber mindestens so schwer wie (E), (0-E) und (TE).
\end{fazit}

% §5. Beschränktheit und Überdeckbarkeit
\section{Beschränktheit und Überdeckbarkeit}

% 5.3
\begin{lem}[\emph{Dickson}]
  $\leq$ ist eine Wohlquasiordnung auf~$(\N \cup \{ \omega \})^n$, \dh{} für alle unendlichen Folgen $(M_i)_{i \in \N}$ in~$(\N \cup \{ \omega \})^n$ gibt es eine Teilfolge $(M_{i_j})_{j \in \N}$ mit $M_{i_j} \leq M_{i_{j+1}}$ für alle $j \in \N$.
\end{lem}

\begin{defn}
  Ein \emph{Weg} in einem Graphen~$(V, E)$ ist eine Folge $v_1 \ldots v_n$ in~$V$ mit $\fa{i \neq j} v_i \neq v_j$ und $(v_i, v_{i+1}) \in E$.
\end{defn}

\begin{defn}
  Ein Graph~$(V, E)$ heißt \emph{lokal endlich}, falls für alle $v \in V$ die Menge $\Set{w \in V}{(v, w) \in E}$ endlich ist.
\end{defn}

\begin{lem}[\emph{König}]
  Sei $(V, E)$ ein unendlicher, lokal endl. gericht. Graph und $v_0 \in V$ ein Knoten, sodass für alle $v \in V$ ein Weg von~$v_0$ nach~$v$ existiert. 
  Dann gibt es einen unendlichen Weg ausgehend von~$v_0$.
\end{lem}

% 5.2
\begin{satz}
  $
    N \text{ ist unbeschränkt} \enspace \iff
    \begin{array}[t]{l}
      \ex{M, M' \in \activeTransition{M_N}} \ex{w \in T^*} \\
      M \activeTransition{w} M' \wedge M \leq M' \wedge M \neq M'
    \end{array}
  $
\end{satz}

% 5.1
\begin{defn}
  Eine \emph{erweiterte Markierung} \textit{von~$N$} ist eine Abbildung
  \[
    M : S \to \N \cup \{ \omega \}.
  \]
\end{defn}

\begin{nota}
  $\ExtMarkings(S) \coloneqq \{ \text{ erw. Mark. von~$N$ } \} \coloneqq (\N \cup \{ \omega \})^S$
\end{nota}

% 5.7
\begin{defn}
  Sei $N$ ein Netz und $M_1$, $M_2$ erweiterte Markierungen.
  \begin{itemize}
    \item $M_2$ \emph{überdeckt} $M_1$ $\coloniff$ $M_1 \leq M_2$
    \item $M_1$ ist \emph{überdeckbar} $\coloniff$ $\ex{M \in \activeTransition{M_N}} M_1 \leq M$
  \end{itemize}
\end{defn}

\begin{defn}
  Eine Menge $S' \subseteq S$ heißt \emph{simultan unbeschränkt}, falls
  \[
    \fa{n \in \N} \ex{M \in \activeTransition{M_N}} \fa{s \in S} M(s) \geq n.
  \]
\end{defn}

\begin{defn}
  Sei $N = (S, T, W, M_N)$ ein Netz.
  Ein \emph{Überdeckungsgraph} von~$N$ ist ein kantenbeschrifteter, gericht. Graph $\Cov(N) = (V, E)$, der von folgendem (nichtdet.) Algorithmus berechnet wird:
  \begin{algorithmic}[1]
    \State{
      $V \coloneqq \emptyset \subset \ExtMarkings(S)$, \enspace
      $A \coloneqq \{ M_N \} \subset \ExtMarkings(S)$,
    }
    \State{
      $E \coloneqq \emptyset \subset \ExtMarkings(S) \times T \times \ExtMarkings(S)$,
    }
    \State{
      $\Call{pred}{} \coloneqq \mathrm{const} \, \nil \in (\ExtMarkings(S) \cup \{\nil\})^{\ExtMarkings(S)}$
    }
    \While{$A \neq \emptyset$}
      \State wähle $M \in A$
      \State $A \coloneqq A \setminus \{ M \}$, \enspace $V \coloneqq V \cup \{ M \}$
      \For{$t \in T$ mit $M \activeTransition{t}$}
        \State $M' \coloneqq M + \Delta t$, \enspace $M^* \coloneqq M$
        \While{$M^* \neq \nil \wedge M^* \not\leq M'$}
          $M^* \coloneqq \Call{pred}{M^*}$
        \EndWhile
        \If{$M^* \neq \nil$}
          $M' \coloneqq M' + \omega \cdot (M' - M^*)$ %= (s \mapsto \max (\{ M'(s) \} \cup \Set{\omega}{M'(s) > M^*(s)}) )
        \EndIf
        \State $E \coloneqq E \cup \{ (M, t, M') \}$
        \If{$M' \not\in V \cup A$}
          $A \coloneqq A \cup \{ M' \}$, \enspace
          $\Call{pred}{M'} \coloneqq M$
        \EndIf
      \EndFor
    \EndWhile
  \end{algorithmic}
\end{defn}

% 5.8
\begin{satz}
  $\Cov(N)$ ist endlich ($\!\iff\!$ der Algorithmus terminiert)
\end{satz}

\begin{kor}
  Es ist entscheidbar, ob~$N$ beschränkt ist.
\end{kor}

\begin{beweis}
  Konstruiere $\Cov(N) = (V, E)$ wobei $V \subset \ExtMarkings(S)$ endl. ist.
  Überprüfe, ob sogar $V \subset \Markings(S)$ gilt.
  Falls ja, so ist $\ReachabilityGraph(N) = \Cov(N)$ endlich.
  Falls nein, so gibt es $M$, $M'$ wie im letzten Satz und~$N$ ist somit unbeschränkt.
\end{beweis}

\begin{bem}
  Jedes $\Cov(N)$ ist (nach Einführen eines Fehlerzustandes und Kanten dorthin) ein determ. endl. Automat mit Startzustand~$M_N$.
\end{bem}

\begin{defn}
  $L(\Cov(N)) \subseteq T^*$ ist die Sprache der von einem $\Cov(N)$ akzeptierten Wörter. 
\end{defn}

\begin{nota}
  $M_w \coloneqq $ durch $w \in L(\Cov(N))$ erreichter Zust. in $\Cov(N)$
\end{nota}

% 5.10 a)
\begin{lem}
  $
    M_N \activeTransition{w} M \enspace \implies
    \begin{array}[t]{l}
      w \in L(\Cov(N)) \wedge \\
      \fa{s \in S} M_w(s) \in \{ M(s), \omega \}
    \end{array}
  $
  % ausgelassen: triviales Korollar
\end{lem}

% 5.11
\begin{lem}
  Für alle $M$ in $\Cov(N)$ u. alle $n \in \N$ gibt es ein $M' \!\in\! \activeTransition{M_N}$ mit
  \[
    \begin{cases}
      M'(s) = M(s) & \text{falls } M(s) \neq \omega, \\
      M'(s) > n & \text{falls } M(s) = \omega.
    \end{cases}
  \]
\end{lem}

% 5.12, 5.13, 5.14
\begin{kor}
  \begin{itemize}
    \item $S'$ ist simultan unbeschränkt $\iff$ $(\mathrm{const} \, \omega) \in \Cov(N)$
    \item Sei $\tilde{M}$ eine Markierung von~$N$. Dann gilt: $\tilde{M}$ ist überdeckbar in~$N$ $\iff$ $\tilde{M}$ wird von einem $M$ in~$\Cov(N)$ überdeckt
    \item $t$ ist 1-lebendig in~$N$ $\iff$ $t$ ist Kantenbeschriftung in $\Cov(N)$
    % Übungsblatt 11, Aufgabe 2a)
    \item $t$ ist 2-lebendig $\iff$ $t$ ist Beschriftung in einem Kreis in $\Cov(N)$
  \end{itemize}
\end{kor}

\begin{kor}
  Es sind anhand von~$\Cov(N)$ entscheidbar:
  \begin{itemize}
    \miniitem{0.48 \linewidth}{Simultane Unbeschränktheit}
    \miniitem{0.48 \linewidth}{Überdeckbarkeit von Markier.}
    \item 1-Lebendigkeit und 2-Lebendigkeit von Transitionen
  \end{itemize}
\end{kor}

\newpage

% §6. Strukturtheorie und Free-Choice-Netze
\section{Strukturtheorie und Free-Choice-Netze}

\begin{konv}
  In diesem Abschn. seien alle Kantengewichte 0 oder~1.
\end{konv}

\begin{defn}
  Eine Teilmenge $R \subseteq S$ heißt
  \begin{itemize}
    \miniitem{0.4 \linewidth}{\emph{Siphon}, falls $\preset{R} \subseteq \postset{R}$}
    \miniitem{0.4 \linewidth}{\emph{Falle}, falls $\postset{R} \subseteq \preset{R}$}
  \end{itemize}
\end{defn}

\begin{lem}
  \begin{itemize}
    \item Ist $R$ ein Siphon und unmarkiert unter~$M$, so ist~$R$ unmarkiert unter allen $M' \in \activeTransition{M}$.
    \item Ist $R$ eine Falle und markiert unter~$M$, so ist~$R$ markiert unter allen $M' \in \activeTransition{M}$.
  \end{itemize}
\end{lem}

% 6.4
\begin{beob}
  Angenommen, $N$ hat keine isolierten Stellen.
  Ist $R \neq \emptyset$ ein Siphon und unmarkiert unter $M \in \activeTransition{M_n}$, so ist~$N$ nicht lebendig.
\end{beob}

% 6.5
\begin{lem}
  Sei $T \neq \emptyset$ und $M$ eine tote Markierung. \\
  Dann ist $R = M^{-1}(\{ 0 \})$ ein nichtleerer, unmarkierter Siphon.
\end{lem}

% 6.6
\begin{lem}
  Sei $T \neq \emptyset$.
  Enthält jeder nichtleere Siphon eine markierte Falle, so ist~$N$ verklemmungsfrei.
\end{lem}

\begin{defn}
  Ein Netz $N$ mit Kantengewichten in $\{ 0, 1 \}$ heißt
  \begin{itemize}
    \item \emph{Free-Choice-Netz} (\textit{FC-Netz}), falls
    \[
      \fa{t, t' \in T} t \neq t' \wedge s \in \preset{t} \cap \preset{t'} \implies \preset{t} = \preset{t'} = \{ s \}.
    \]
    \item \emph{erweitertes Free-Choice-Netz} (\textit{EFC-Netz}), falls
    \[
      \fa{t, t' \in T} \preset{t} \cap \preset{t'} \neq \emptyset \implies \preset{t} = \preset{t'}.
    \]
  \end{itemize}
\end{defn}

% 6.8
\begin{bem}
  Ist $N$ ein EFC-Netz, $s \in S$, $t_1, t_2 \in \postset{s}$ und~$M$ eine Markierung, so gilt $M \activeTransition{t_1} \iff M \activeTransition{t_2}$.
\end{bem}

% 6.9
\begin{lem}
  Die Vereinigung von Siphons / Fallen ist wieder ein Siphon / eine Falle.
  Damit bilden Siphons / Fallen mit der Vereinigung einen beschränkten Halbverband.
\end{lem}

% 6.9
\begin{kor}
  \begin{itemize}
    \item Jedes $R \subseteq S$ enthält eine größte Falle.
    \item $R \subseteq S$ enthält eine markierte Falle $\iff$ die größte Falle in~$R$ ist markiert
  \end{itemize}
\end{kor}

\begin{defn}
  Sei $P \subseteq S$ und ${<}$ eine Totalordnung auf~$P$.
  Die durch ${<}$ induzierte \emph{lexikographische Ordnung}~${<_\mathrm{lex}}$ auf~$\Markings(S)$ ist
  \[
    M_1 <_\mathrm{lex} M_2 \coloniff \ex{p \in P}
    \begin{array}[t]{r l}
      & \fa{q < p} M_1(q) = M_2(q) \\
      \wedge & M_1(p) < M_2(p).
    \end{array}
  \]
\end{defn}

% 6.10
\begin{lem}
  $<_\mathrm{lex}$ ist Noethersch (wohlfundiert)
\end{lem}

% 6.11
\begin{lem}
  Sei $N$ ein EFC-Netz, $R \subseteq S$ und $Q \subseteq R$ die größte Falle in~$R$.
  Dann gibt es eine Totalordnung~${<}$ auf $R \setminus Q$, sodass: \\[0.2em]
  Für alle Markierungen $M$ mit $M|_Q \equiv 0$ und $\ex{t \in \postset{R}} M \activeTransition{t}$ gilt
  \[
    \ex{M' \in \activeTransition{M}} M' <_\mathrm{lex} M \wedge M'|_Q \equiv 0.
  \]
\end{lem}

\begin{beweis}
  Setze $n \coloneqq \card{R \setminus Q}$.
  Wähle
  \begin{itemize}
    \item $t_1 \in \postset{R} \setminus \preset{R}$ und $s_1 \in \preset{t_1} \cap (R \setminus Q)$
    \item $t_2 \in \postset{(R \setminus \{ s_1 \})} \setminus \preset{(R \setminus \{ s_1 \})}$ und $s_2 \in \preset{t_1} \cap (R \setminus (Q \cup \{ s_1 \}))$
    \item \ldots
    \item $t_n \in \postset{(R \setminus \{ s_1, \ldots, s_{n-1} \})} \setminus \preset{(R \setminus \{ s_1, \ldots, s_{n-1} \})}$ und $s_n \in \preset{t_1} \cap (R \setminus (Q \cup \{ s_1, \ldots, s_{n-1} \}))$
  \end{itemize}
  Definiere ${<}$ durch $s_n < \ldots < s_2 < s_1$.
  Für~$t$ mit $M \activeTransition{t}$ gibt es ein maximales $i \in \{ 1, \ldots, n \}$ mit $s_i \in \preset{t}$.
  Da~$N$ EFC ist, gilt $\preset{t_i} = \preset{t}$. \\
  Somit existiert~$M'$ mit $M \activeTransition{t_i} M'$.
  Es stimmen $M$ und $M'$ auf $Q \cup \{ s_{i+1}, \ldots, s_n \}$ überein, aber $M'(s_i) < M(s_i)$.
  Also $M' <_\mathrm{lex} M$.
\end{beweis}

% 6.11
\begin{kor}
  Die Aussage des letzten Satzes gilt auch für alle Markierungen~$M$ mit $M|_Q \equiv 0$ und $\ex{t \in \postset{R}}$ $t$ ist 1-lebendig unter~$M$, falls~$R$ ein Siphon ist.
\end{kor}

\begin{satz}[\emph{Commoner}]
  Sei $N$ ein EFC-Netz ohne isol. Stellen.
  Dann:
  \[
    \text{$N$ ist lebendig $\iff$ jeder Siphon $\neq \emptyset$ enth. eine markierte Falle}
  \]
\end{satz}

\begin{beweis}
  "`$\Rightarrow$"'.
  Sei $R$ ein nichtleerer Siphon und $Q \subseteq R$ die größte Falle in~$R$.
  Wähle $t \in \postset{R}$.
  Angenommen, $M_N|_Q \equiv 0$.
  Durch mehrmalige Anwendung des vorh. Korollar (beachte: $t$ ist lebendig) erhalten wir eine unendliche absteigende Reihe $M_N >_\mathrm{lex} M_1 >_\mathrm{lex} \ldots$ im Widerspruch zur Noetherianität von ${<_\mathrm{lex}}$.
  
  "`$\Leftarrow$"'.
  Angenommen, $t_0$ ist nicht lebendig.
  Wir können o.\,B.\,d.\,A. annehmen, dass $t_0$ tot und alle weiteren Transitionen entweder lebendig oder tot sind.
  Zeige: Für jede tote Transition $t$ ist
  \[
    R(t) \coloneqq \Set{s \in \preset(t)}{M_N(s) = 0 \wedge \fa{t' \in \preset{s}} t' \text{ tot}}
  \]
  nichtleer.
  Wir definieren:
  \[
    T_R^{(0)} \coloneqq \{ t_0 \}, \enspace
    R^{(i)} \coloneqq {\bigcup}_{t \in T_R^{(i)}} R(t), \enspace
    T_R^{(i+1)} \coloneqq T_R^{(i)} \cup {\bigcup}_{s \in R^{(i)}} \preset{s}
  \]
  Dann ist $R \coloneqq {\bigcup}_{i \geq 0} R^{(i)}$ ein unmarkierter Siphon.
  Somit sind auch alle Fallen in~$R$ unmarkiert (und immer unmarkiert gewesen).
\end{beweis}

\begin{samepage}

\begin{kor}
  Jedes lebendige EFC-Netz ist monoton lebendig.
\end{kor}

% §7. Netzvariationen
\section{Netzvariationen}

\end{samepage}

% §7.1. High-level-Netze

\begin{defn}
  Ein \emph{High-Level-Netz}~$N$ ist gegeben durch
  \begin{itemize}
    \item eine endliche Menge $S$ von \textit{Stellen},
    \item eine endliche Menge $T$ von \textit{Transitionen},
    \item eine Menge $L$ von \textit{Marken} (eine \textit{Markierung} von~$N$ ist gegeben durch eine Multimenge von~$L$ für jede Stelle von~$N$, also durch eine Abbildung in $\Multisets(L)^S$)
    \item für jede Transition $t \in T$ eine (berechenbare) \textit{Transitionsregel} $r_t \subseteq \Multisets(S \times L) \times \Multisets(S \times L)$
    \item und eine \textit{Anfangsmarkierung} $M_N : S \to \Multisets(L)$.
  \end{itemize}
\end{defn}

% §7.2. Netze mit Zeit

\begin{defn}
  Ein \emph{Netz mit Zeit} ist ein Tupel $N = (S, T, W, M_N, \tau)$, wobei
  \begin{itemize}
    \item $(S, T, W, M_N)$ ein sicheres Petrinetz ist mit $\fa{t \in T} \preset{t} \neq \emptyset$ und
    \item $\tau : T \to \N$ die \emph{Latenzzeit} aller Transitionen angibt.
  \end{itemize}
  Ein \emph{Zustand} von~$N$ ist ein Tupel $(M, \resTime)$, wobei~$M$ eine Markierung ist und $\resTime : T \to \N \cup \{ \infty \}$ die \textit{Restzeit} jeder Transition angibt.
  Es gibt zwei verschiedene Schaltschritte:
  \begin{align*}
    (M, \resTime) \activeTransition{\sigma} (M, \resTime') & \coloniff
    \resTime \geq 1 \wedge \resTime' = \resTime - 1 \tag{\emph{Zeitschritt}} \\
    (M, \resTime) \activeTransition{t} (M', \resTime') & \coloniff
    M \activeTransition{t} M' \wedge \tag{\emph{Transition}} \\
    & \wedge \resTime'(t') = \begin{cases}
      \tau(t') & \text{falls $\neg (M \activeTransition{t'}) \wedge M' \activeTransition{t'}$} \\
      \resTime(t') & \text{falls $M \activeTransition{t'} \wedge M' \activeTransition{t'}$} \\
      \infty & \text{falls $\neg (M' \activeTransition{t'})$}
    \end{cases}
  \end{align*}
  Der Anfangszustand ist $(M_N, \resTime_N)$, wobei
  \[
    \resTime_N(t) \coloneqq \begin{cases}
      \tau(t) & \text{falls } M_N \activeTransition{t} \\
      \infty & \text{falls } \neg (M_N \activeTransition{t})
    \end{cases}
  \]
\end{defn}

% §7.3 Netze mit Prioritäten

\begin{defn}
  Ein \emph{Netz mit Prioritäten} ist ein Petri-Netz $N = (S, T, W, M_N)$ mit einer Halbordnung ${\sqsubset}$. \\
  Das Netz \textit{schaltet unter Beachtung der Priorität}, falls
  \[
    M \activeTransition{t}_{\sqsubset} M' \coloniff M \activeTransition{t} M' \wedge \fa{t' \in T} M \activeTransition{t'} \implies t' \not\sqsubset t
  \]
\end{defn}

% §7.4 Netze mit Inhibitor-Kanten

\begin{defn}
  Ein \emph{Netz mit Inhibitor-Kanten} ist ein Petri-Netz $N = (S, T, W, M_N)$ zusammen mit einer Menge $I \subseteq S \times T$ von \textit{Inhibitor-Kanten}.
  Man definiert:
  \[
    M \activeTransition{t}_I M' \coloniff M \activeTransition{t} M' \wedge \fa{s \in S} (s, t) \in I \implies M(s) = 0
  \]
\end{defn}

\begin{defn}
  Eine \emph{Zählermaschine} besteht aus $\N$-wertigen Registern $c_1, \ldots, c_n$ und einem Programm bestehend aus den Instruktionen
  \begin{itemize}
    \item $\Call{incr}{c_i}$ -- erhöhe $c_i$ um eins
    \item $\Call{jzdec}{c_i, m}$ -- springe zu Adresse $m$, falls $c_i = 0$, ansonsten erniedrige $c_i$ um eins.
  \end{itemize}
\end{defn}

\begin{prop}
  Für jede Turingmaschine gibt es eine 2-Zählermaschine, die die Turingmaschine simuliert (bei passender Kodierung der Eingabe und Ausgabe).
\end{prop}

\begin{kor}
  Das Halteproblem für 2-Zählermaschinen ist unentscheidbar.
\end{kor}

\begin{lem}
  Zählermaschinen lassen sich als Netze mit Zeit, mit Prioritäten oder mit Inhibitor-Kanten kodieren.
\end{lem}

\begin{kor}
  Das Erreichbarkeitsproblem ist für solche Netze unentscheidbar.
\end{kor}

% §7.6 Kapazitäten

\begin{defn}
  Ein \emph{Netz mit Kapazitäten} ist ein Petri-Netz $N = (S, T, W, M_N)$ zusammen mit einer Abbildung $k : S \to \N \cup \{ \infty \}$.
  Man definiert:
  \[
    M \activeTransition{t}_k M' \coloniff M \activeTransition{t} M' \wedge M' \leq k
  \]
\end{defn}

% §8 Nichtdeterminismus und modulare Konstruktion
\section{Nichtdeterminismus und modulare Konstruktion}

% 8.1
\begin{defn}
  Zwei Netze $N_1$ und $N_2$ heißen \emph{sprachäquivalent}, wenn
  \[
    N_1 \sim_L N_2 \coloniff L(N_1) = L(N_2).
  \]
\end{defn}

% 8.2
\begin{satz}
  Für beschränkte Netze ist Sprachäquivalenz entscheidbar.
\end{satz}

\begin{beweis}
  Für beschränkte Netze~$N$ ist $L(N)$ regulär (man erhält einen endlichen Automaten aus~$\ReachabilityGraph(N)$).
  Gleichheit von regulären Sprachen ist entscheidbar.
\end{beweis}

\begin{bem}
  Sprachäquivalenz ist unzureichend für den Systemvergleich, denn es interessiert nicht nur, welche Aktionen ein Netz hintereinander ausführen kann, sondern auch in welchem Zustand es sich danach befindet und insbesondere welche Aktionen es dann in der Zukunft ausführen kann.
\end{bem}

% 8.3
\begin{defn}
  Die \emph{ready-Semantik} eines Netzes~$N$ ist
  \[
    \ready(N) \coloneqq \Set{(w, X)}{\ex{M} M_N \labelledTransition{w} M \wedge X = \Set{a \in \Sigma}{M \labelledTransition{a}}}.
  \]
  $N_1$, $N_2$ heißen \emph{ready-äquivalent}, falls $\ready(N_1) = \ready(N_2)$.
\end{defn}

% 8.4
\begin{defn}
  Die \emph{Failure-Semantik} (\textit{Verweigerungssemantik}) eines Netzes~$N$ ist
  \[
    \Failure(N) \coloneqq \Set{(w, X)}{X \subseteq \Sigma, \ex{M} M_N \labelledTransition{w} M \wedge \fa{a \in X} \neg M \labelledTransition{a}}.
  \]
  Dabei heißt~$X$ \textit{Verweigerungsmenge}. \\
  $N_1$, $N_2$ sind \emph{failure-äquivalent} ($\Failure$-äquivalent), falls
  \[
    N_1 \sim_\Failure N_2 \coloniff \Failure(N_1) = \Failure(N_2).
  \]
\end{defn}

% 8.5
\begin{lem}
  \begin{itemize}
    \item $(w, X) \in \Failure(N), Y \subseteq X \implies (w, Y) \in \Failure(N)$
    \item $(w, \emptyset) \in \Failure(N) \iff w \in L(N)$
    \item $(w, X) \in \Failure(N), \fa{a \in Y} (wa, \emptyset) \not\in L(N) \implies (w, X \cup Y) \in \Failure(N)$
    \item $(w, X) \in \Failure(N), Y \subseteq \Sigma \setminus \ell(T) \implies (w, X \cup Y) \in \Failure(N)$
  \end{itemize}
\end{lem}

\begin{lem}
  $
    (w, X) \in \Failure(N) \iff \ex{Y \subseteq \Sigma \setminus X} (w, Y) \in \ready(N)
  $
\end{lem}

% 8.6
\begin{satz}
  Ready-Äquivalenz $\implies$ $\Failure$-Äquivalenz $\implies$ Sprachäquivalenz
\end{satz}

\begin{bem}
  Die Umkehrungen sind falsch.
\end{bem}

% 8.7, erweitert um Ready-Äquivalenz
\begin{satz}
  Für beschränkte Netze ist Ready- und $\Failure$-Äquiv. entscheidbar.
\end{satz}

\begin{beweisidee}
  Aus jedem Netz~$N$ kann man einen endlichen Automaten konstruieren, dessen Sprache kanonisch isomorph zu~$\ready(N)$ bzw. $\Failure(N)$ ist.
  Gleichheit von regulären Sprachen ist entscheidbar.
\end{beweisidee}

% Ausgelassen: Semi-formale Definition von Kompositionalität von Semantiken

% 8.8
\begin{defn}
  Seien $N_1$ und $N_2$ mit~$\Sigma$ beschriftete Petrinetze und $A \subseteq \Sigma$.
  Die \emph{parallele Komposition} \textit{mit Synchronisation über~$A$} ist das beschriftete Netz $N \parallelComposition_A N_2 = (S, T, W, M_N, \ell)$ mit
  \begin{itemize}
    \item $S = S_1 \amalg S_2$
    \item
      $
        T =
        \begin{array}[t]{r l}
          & \Set{(t_1, \lambda)}{t_1 \in T_1, \ell_1(t_1) \not\in A} \\
          \amalg & \Set{(\lambda, t_2)}{t_2 \in T_2, \ell_2(t_2) \not\in A} \\
          \amalg & \Set{(t_1, t_2) \in T_1 \times T_2}{\ell_1(t_1) = \ell_2(t_2) \in A}
        \end{array}
      $
      \item
        $
          \begin{array}[t]{r c l}
            W(s_1 \in S_1, (t_1, t_2)) &\coloneqq& W_1(s_1, t_1) \enspace \text{falls $t_1 \in T_1$} \\
            W(s_2 \in S_1, (t_1, t_2)) &\coloneqq& W_2(s_2, t_2) \enspace \text{falls $t_2 \in T_2$} \\
            W(s \in S, t \in T) &\coloneqq& 0 \enspace \text{(sonst)} \\
            W((t_1, t_2), s_1 \in S_1) &\coloneqq& W_1(t_1, s_1) \enspace \text{falls $t_1 \in T_1$} \\
            W((t_1, t_2), s_2 \in S_1) &\coloneqq& W_2(t_2, s_2) \enspace \text{falls $t_2 \in T_2$} \\
            W(t \in T, s \in S) &\coloneqq& 0 \enspace \text{(sonst)}
          \end{array}
        $
        \item $M_N \coloneqq M_{N_1} \amalg M_{N_2}$
        \item
          $
            \begin{array}[t]{r c l}
              \ell((t_1, t_2) \in T_1 \times T_2) &\coloneqq& \ell_1(t_1) = \ell_2(t_2) \\
              \ell(t_1 \in T_1) &\coloneqq& \ell_1(t_1) \\
              \ell(t_2 \in T_2) &\coloneqq& \ell_2(t_2) \\
            \end{array}
          $
  \end{itemize}
\end{defn}

\begin{bem}
  Die Menge der mit~$\Sigma$ beschr. Netze wird mit $\parallelComposition_A$ zu einem komm. Monoid mit neutralem Element $(S = \emptyset, T = \Sigma, \blank, \blank, \ell = \id)$
\end{bem}

% 8.9
\begin{lem}
  Sei $N = N_1 \parallelComposition N_2$, $M_1, M_1' \in \Markings(S_1)$, $M_2, M_2' \in \Markings(S_2)$ und $(t_1^{(1)}, t_2^{(1)}), \ldots, (t_1^{(n)}, t_2^{(n)}) \in T_N$.
  Dann gilt:
  \begin{align*}
    & M_1 \amalg M_2 \activeTransition{(t_1^{(1)}, t_2^{(1)}), \ldots, (t_1^{(n)}, t_2^{(n)})} M_1' \amalg M_2' \\
    \iff & M_1 \activeTransition{t_1^{(1)}, \ldots, t_1^{(n)}} M_1' \wedge
    M_2 \activeTransition{t_2^{(1)}, \ldots, t_2^{(n)}} M_2'
  \end{align*}
\end{lem}

\begin{bem}
  Dabei gilt $M \activeTransition{\lambda} M$ immer.
\end{bem}

% 8.10
\begin{lem}
  Sei $a \in \Sigma \cup \{ \lambda \}$.
  Es gilt $M_1 \amalg M_2 \labelledTransition{a} M_1' \amalg M_2'$ g.\,d.\,wenn
  \begin{itemize}
    \item Falls $a \in A$: \enspace $M_1 \labelledTransition{a} M_1' \wedge M_2 \labelledTransition{a} M_2'$
    \item Falls $a \not\in A$: \enspace $M_1 \labelledTransition{a} M_1' \wedge M_2 \labelledTransition{\lambda} M_2'$ oder $M_1 \labelledTransition{\lambda} M_1' \wedge M_2 \labelledTransition{a} M_2'$
  \end{itemize}
\end{lem}

% 8.11
\begin{defn}
  Seien $u, v \in \Sigma^*$.
  Dann ist
  \[
    \arraycolsep=0.4pt
    u \parallelComposition_A v \coloneqq
      \left\{
        \begin{array}{r l}
          w &= w_1 \cdots w_n \\
          &\in \Sigma^*
        \end{array}
      \,\middle|\,
        \begin{array}{l}
          u = u_1 \cdots u_n, v = v_1 \cdots v_n \text{ mit } \\
          u_i, v_i \in \Sigma \cup \{ \lambda \} \text{ sodass } \\
          \fa{1 \leq i \leq n} u_i = v_i = w_i \in A \\
          \qquad \vee u_i v_i = w_i \not\in A
        \end{array}
      \right\}
  \]
\end{defn}

\begin{bem}
  Im Fall $u_i v_i = w_i$ gilt $u_i = \lambda$ oder $v_i = \lambda$.
\end{bem}

% 8.12
\begin{lem}
  Es sind äquivalent:
  \begin{itemize}
    \item in $N_1 \parallelComposition_A N_2$ gilt $M_1 \amalg M_2 \labelledTransition{w} M_1' \amalg M_2'$
    \item $\ex{u, v \in \Sigma^*} M_1 \labelledTransition{u} M_1' \wedge M_2 \labelledTransition{v} M_2' \wedge w \in u \parallelComposition_A v$
  \end{itemize}
\end{lem}

% 8.13
\begin{satz}
  \begin{itemize}
    \item $L(N_1 \parallelComposition_A N_2) = \cup \Set{u \parallelComposition_A v}{u \in L(N_1), v \in L(N_2)}$
    \item
      $
        \Failure(N_1 \parallelComposition_A N_2) =
        \left\{
        (w, Z)
        \,\middle|\,
        \begin{array}{l}
          \ex{(u, X) \in \Failure(N_1), (v, Y) \in \Failure(N_2)} \\
          w \in u \parallelComposition_A v \text{ und } \\
          Z \cap A \subseteq X \cup Y \text{ und } Z \setminus A \subseteq X \cap Y
        \end{array}
        \right\}
      $
  \end{itemize}
\end{satz}

\begin{kor}
  Sprach- und $\Failure$-Äquivalenzen sind Kongruenzen bzgl.~$\parallelComposition_A$, \dh{}
  \begin{align*}
    N_1 \sim_L N_1', \, N_2 \sim_L N_2' &
    \implies (N_1 \parallelComposition_A N_2) \sim_L (N_1' \parallelComposition_A N_2') \\
    N_1 \sim_\Failure N_1', \, N_2 \sim_\Failure N_2' &
    \implies (N_1 \parallelComposition_A N_2) \sim_\Failure (N_1' \parallelComposition_A N_2')
  \end{align*}
\end{kor}

% TODO: Ready-Äquivalenz ist auch eine Kongruenz, oder?

\begin{bem}
  Dies ist wichtig für den modularen Entwurf von Systemen.
\end{bem}

% 8.15
\begin{defn}
  Ein \textit{beschriftetes} Netz heißt \emph{verklemmungsfrei}, wenn
  \[
    \fa{M \in \activeTransition{M_N}} \ex{a \in \Sigma} M \labelledTransition{a}.
  \]
  Zwei Netze heißen \emph{v-äquivalent}, falls beide verklemmungsfrei oder beide nicht verklemmungsfrei sind.
\end{defn}

% 8.17
\begin{lem}
  $N$ ist verklemmungsfrei $\iff$ $\fa{w \in \Sigma^*} (w, \Sigma) \not\in \Failure(N)$
\end{lem}

% 8.16
\begin{defn}
  Zwei Netze $N_1$ und $N_2$ heißen \emph{VA-äquivalent}, falls: \\[0.4em]
  \hfill\begin{minipage}{0.95 \linewidth}
    Für alle Netze~$N$ und alle $A \subseteq \Sigma$ gilt: \\
    Die Netze $N_1 \parallelComposition_A N$ und $N_2 \parallelComposition_A N$ sind v-äquivalent.
  \end{minipage}
\end{defn}

\begin{bem}
  Offensichtlich ist VA-Äquivalenz eine Kongruenz bzgl.~$\parallelComposition_A$.
\end{bem}

% 8.18
\begin{satz}
  $\Failure$- und VA-Äquivalenz stimmen überein.
\end{satz}

\begin{beweisidee}
  Seien $N_1$ und $N_2$ VA-äquivalent. \\
  Setze $A \coloneqq (\ell_1(T_1) \cup \ell_2(T_2)) \setminus \{ \lambda \}$.
  Zeige: \\
  Für alle $(w, X) \in A^* \times \Powerset(A)$ gibt es ein Netz~$N_{w,X}$, sodass für alle~$N'$ mit $l'(N') \setminus \{ \lambda \} \subseteq A$ gilt:
  \[
    N_{w,X} \parallelComposition_A N' \text{ ist verklemmungsfrei} \iff (w, X) \not\in \Failure(N')
  \]
  Dann gilt für alle $(w, X)$ mit $N \coloneqq N_{w,X}$:
  \[
    \begin{array}{c c c}
      (w, X) \not\in \Failure(N_1)
      && 
      (w, X) \not\in \Failure(N_2) \\
      \Updownarrow && \Updownarrow \\
      N \parallelComposition_A N_1 \text{ verklemmungsfrei}
      & \iff &
      N \parallelComposition_A N_2 \text{ verklemmungsfrei}
    \end{array}
  \]
  \begin{align*}
  \end{align*}
\end{beweisidee}

\end{document}