ENS3
Transcript of ENS3
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 1/13
Grundsatzliche Situationen
Kausalrelation (Fall 1)
t 1
t 2
t •1 ∩•t 2 = ∅ t 2 kann erst nach t 1 schalten.
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 1 / 13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 2/13
Grundsatzliche Situationen
Kausalrelation (Fall 2)
t 1
t 2
t •1 ∩•t 2 = ∅ t 1 kann erst nach t 2 schalten.
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 2 / 13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 3/13
Grundsatzliche Situationen
Konflikt (Fall 1)
t 1
t 2
•t 1 ∩ •t 2 = ∅
Das Schalten von t 1 deaktiviertt 2 und umgekehrt.
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 3 / 13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 4/13
Grundsatzliche Situationen
Konflikt (Fall 2)
t 1
t 2
t •
1
∩ t •
2
= ∅
Das Schalten von t 1 deaktiviertt 2 und umgekehrt.
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 4 / 13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 5/13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 6/13
Unabhangige Transitionen
Sei ENS = (S ,T ,F ,M 0) ein elementares Netzsystem.
Eine Transitionsmenge U ⊆ T heißt unabhangig, falls(•t 1 ∪ t •1 ) ∩ (•t 2 ∪ t •2 ) = ∅ f ur alle t 1, t 2 ∈ U mit t 1 = t 2.
U heißt M -aktiviert, falls gilt:
(1) •U ⊆ M (2) U • ∩M = ∅
mit •
U = t ∈U
•
U und U •
= t ∈U
t
•
.
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 6 / 13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 7/13
Parallelschaltung
Sei ENS = (S ,T ,F ,M 0) ein elementares Netzsystem.
Eine Teilmenge U ⊆ T heißt parallele Transition.
U schaltet parallel von M nach M , in Zeichen M [U M , falls gilt
(1) U ist unabhangig,(2) U ist M -aktiviert,(3) M = (M −•U ) ∪ U •.
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 7 / 13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 8/13
Sequentalisierungssatz
Seien
ENS = (S ,T ,F ,M 0) ein elementares Netzsystem,
M ,M ⊆ S zwei Markierungen von ENS ,
U ,U 1,U 2 ⊆ T mit U 1 ∪ U 2 = U und U 1 ∩ U 2 = ∅.
Dann gilt:
M [U M impliziert M [U 1M 1[U 2M
f ur die Markierung M 1 = (M − •U 1) ∪ U •1 ⊆ S .
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 8 / 13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 9/13
Beweis
Die Korrektheit des Sequentialisierungssatzes ergibt sich aus den folgendenBeobachtungen:
1 U 1 ist M -aktiviert, d.h., •U 1 ⊆ M und U •1 ∩M = ∅.
2 U 2 ist M 1-aktiviert, d.h., •U 2 ⊆ M 1 und U •2 ∩M 1 = ∅.
3 (M − •U ) ∪ U • = (M 1 − •U 2) ∪ U •2 .
Beweis von Beobachtung 1
Wegen •U 1 ⊆ •U ⊆ M gilt •U 1 ⊆ M und wegen U •1 ⊆ U • und U • ∩M = ∅
gilt auch U •1 ∩M = ∅.
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 9 / 13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 10/13
Beweis von Beobachtung 2
Nach Voraussetzung gilt •
U 2 ⊆ M −•
U 1 und somit •
U 2 ⊆ (M −•
U 1) ∪ U
•
1 ,d.h., •U 2 ⊆ M 1. Ebenfalls nach Voraussetzung gilt U •2 ∩M = ∅, also auchU •2 ∩ (M − •U 1) = ∅. Wegen U •1 ∩ U •2 = ∅ erhalten wirU •2 ∩ ((M − •U 1) ∪ U •1 ) = ∅, d.h., U •2 ∩M 1 = ∅.
Beweis von Beobachtung 3(M − •U ) ∩ U •
= (M − (•U 1 ∪ •U 2)) ∪ (U •1 ∪ U •2 )= (((M − •U 1) − •U 2) ∪ U •1 ) ∪ U •2
=∗
(((M −•
U 1) ∪ U
•
1 ) −•
U 2) ∪ U
•
2= (M 1 − •U 2) ∪ U •2
* Wegen •U 2 ∩ U •1 = ∅
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 10 / 13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 11/13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 12/13
Bemerkung 2
Wendet man den Sequentialisierungssatz solange an, bis jedeTransitionsmenge genau ein Element enthalt, ergibt sich f ur jedebeliebige Reihenfolge w der Transitionen in U :
M [w M
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 12 / 13
7/25/2019 ENS3
http://slidepdf.com/reader/full/ens3 13/13
Parallelisierungssatz
Sei U eine Menge von Transitionen und seien M ,M Markierungen, sodass M [w M f ur jede beliebige Reihenfolge w der Transitionen in U .Dann gilt:
M [U M .
Das heißt, die Transitionen in U k¨onnen parallel geschaltet werden, falls sie
in jeder beliebigen Reihenfolge geschaltet werden konnen.
Sabine Kuske (Universitat Bremen, Informatik) Petri-Netze, WS 2015/2016 13 / 13