2.6 Petrinetze
89
Formal kann dies wie folgt definiert werden:
Definition 2.22: Transition t ∈ T heißt M-aktiviert, wenn sie die folgende komplexe
Bedingung erfüllt:
(∀p ∈
• t : M(p) ≥ W(p, t)) ∧ (∀p
′ ∈ t
• : M(p
′ ) + W(t, p
′ ) ≤ K(p
′ ))
Aktivierte Transitionen können schalten, müssen dies aber nicht zwangsläufig. Wenn
mehrere Transitionen aktiviert sind, ist die Reihenfolge ihres Schaltens nicht deterministisch definiert.
Der Einfluss einer schaltenden Transition t auf die Markenzahl kann bequem
durch einen der Transition zugeordneten Vektor t beschrieben werden, der wie folgt
definiert ist:
t(p) =
−W(p, t),
falls p ∈ • t \ t •
+W(t, p),
falls p ∈ t • \ • t
−W(p, t) + W(t, p), falls p ∈ • t ∩ t •
0
sonst
Beim Schalten einer Transition t ergibt sich dann die neue Markenzahl M ′ für alle
Stellen p wie folgt:
M
′ (p) = M(p) + t(p)
Unter Benutzung der Vektoraddition können wir verkürzt schreiben:
M
′ = M + t
Aus der Menge aller Vektoren können wir eine sogenannte Inzidenzmatrix N bilden,
welche als Spalten die Vektoren der verschiedenen Transitionen enthält:
N : P × T → Z; ∀t ∈ T : N(p, t) = t(p)
Mit Hilfe dieser Matrix kann man auf standardisierte Weise formale Beweise von
Systemeigenschaften führen. Beispielsweise kann es Teilmengen der Stellen geben,
in denen sich die Gesamtzahl der Marken unabhängig von den schaltenden Transitionen nicht verändert [468]. Solche Stellenmengen konstanter Markensumme nennen
wir S-Invarianten. Um solche S-Invarianten zu finden, betrachten wir zunächst eine
Transition t j und suchen Stellenmengen R ⊆ P, für die das Schalten der Transition
die Markenzahl nicht verändert. Für diese muss gelten:
p ∈R
t j (p) = 0
(2.14)
Abbildung 2.51 zeigt ein Beispiel für eine Transition, bei der für die drei Stellen
die Markensumme konstant bleibt.
89
Formal kann dies wie folgt definiert werden:
Definition 2.22: Transition t ∈ T heißt M-aktiviert, wenn sie die folgende komplexe
Bedingung erfüllt:
(∀p ∈
• t : M(p) ≥ W(p, t)) ∧ (∀p
′ ∈ t
• : M(p
′ ) + W(t, p
′ ) ≤ K(p
′ ))
Aktivierte Transitionen können schalten, müssen dies aber nicht zwangsläufig. Wenn
mehrere Transitionen aktiviert sind, ist die Reihenfolge ihres Schaltens nicht deterministisch definiert.
Der Einfluss einer schaltenden Transition t auf die Markenzahl kann bequem
durch einen der Transition zugeordneten Vektor t beschrieben werden, der wie folgt
definiert ist:
t(p) =
−W(p, t),
falls p ∈ • t \ t •
+W(t, p),
falls p ∈ t • \ • t
−W(p, t) + W(t, p), falls p ∈ • t ∩ t •
0
sonst
Beim Schalten einer Transition t ergibt sich dann die neue Markenzahl M ′ für alle
Stellen p wie folgt:
M
′ (p) = M(p) + t(p)
Unter Benutzung der Vektoraddition können wir verkürzt schreiben:
M
′ = M + t
Aus der Menge aller Vektoren können wir eine sogenannte Inzidenzmatrix N bilden,
welche als Spalten die Vektoren der verschiedenen Transitionen enthält:
N : P × T → Z; ∀t ∈ T : N(p, t) = t(p)
Mit Hilfe dieser Matrix kann man auf standardisierte Weise formale Beweise von
Systemeigenschaften führen. Beispielsweise kann es Teilmengen der Stellen geben,
in denen sich die Gesamtzahl der Marken unabhängig von den schaltenden Transitionen nicht verändert [468]. Solche Stellenmengen konstanter Markensumme nennen
wir S-Invarianten. Um solche S-Invarianten zu finden, betrachten wir zunächst eine
Transition t j und suchen Stellenmengen R ⊆ P, für die das Schalten der Transition
die Markenzahl nicht verändert. Für diese muss gelten:
p ∈R
t j (p) = 0
(2.14)
Abbildung 2.51 zeigt ein Beispiel für eine Transition, bei der für die drei Stellen
die Markensumme konstant bleibt.