-
Zur Startseite
Zum Editor

Zum Tutorial

PetriEdiSim

Tutorial zum Thema "Petri-Netze"
2.   Petri-Netze
2.5   Analyse von Netzen



Vorheriges Kapitel    Nächstes Kapitel

2.5   Analyse von Netzen

Die Analyse von Netzen wird im folgenden anhand dieses Beispielnetzes erfolgen. Alle Erläuterungen dieses Kapitels beziehen sich auf das Netz N1.

Beispielnetz :
MUTEX = Dieses Netz MUTEX ist als Beispielnetz Nr.4 in dem Editor vorhanden und kann simuliert werden !!.



Mit Hilfe dieses Netzes sollen folgende Eigenschaften nachgewiesen werden :

(1) Wechselseitiger Ausschluß
Es ist niemals gleichzeitig ein Token in p3 und p7.
(2) Sicherheit des Netzes
Es liegen niemals mehr als ein Token in einem Platz pi.



Dazu muß die Menge mark(N1) untersucht werden. Es wird hier ein systematischer Ansatz vorgestellt : die Methode der S-Invarianten.

Im folgenden wird stets ein Netz der N = ( A, Pl, ->0, M0 ) mit endlicher Platzmenge Pl betrachtet.
Die Transition t ->0 und die Markierungen M von N werden als Vektoren dargestellt :

t = Pl ->     ( hier genügt { -1, 0, 1 } )
wobei

t( p ) =    1      falls p post(t) - pre(t)
-1      falls p pre(t) - post(t)
   0      sonst

Hierbei ist zu beachten, daß der letzte Fall t( p ) = 0 insbesondere bei sogenannten Schlingen im Netz auftritt, d.h. falls

p pre(t) post(t) gilt, z.B.



Markierungen M sind definitionsgemäß von der Form

M : Pl -> IN0

Für Vektoren A, B : Pl -> gibt es die aus der Linearen Algebra bekannten Operatoren :

· Vektoraddition
A + B mit (A + B)( p ) = A( p ) + B( p )

· Produkt mit Skalaren c
c · A mit (c · A)( p ) = c · A( p )

· Skalarprodukt
A · B = A( p ) · B( p )


  Anfang der Seite


Es gelten die bekannten Rechengesetze, z.B. gilt für alle A, B, C : Pl ->

( A + B ) · C = A · C + B · C

Vektoren können als Spalten dargestellt werden.


Beispiel :
Die Anfangsmarkierung M0 von MUTEX kann als Spalte dargestellt werden.


p M0
p1
p2
p3
p4
p5
p6
p7
p1 1
p0 1
p0 1
p0 1
p1 1
p0 1
p0 1



Definition :
(Matrizendarstellung von Netzen)
Jedes Netz N = ( A , Pl , ->0 , M0 ) mit endlicher Platzmenge Pl läßt sich als endliche Matrix

N : ( Pl     × ->0 ) ->     (hier { -1, 0, 1 })

darstellen :

N (p , t ) = t( p )


Anschaulich besteht N aus den Transitionsvektoren als Spalten :

N t1 . . . tn
p1
.
.
.
pm
. . . . .



Beispiel :
MUTEX sieht in Matrizendarstellung wie folgt aus :


MUTEX n1 b1 e1 n2 b2 e2
p1
p2
p3
p4
p5
p6
p7
p-1 1
p-1 1
p-0 1
p-0 1
p-0 1
p-0 1
p-0 1
p-0 1
p-1 1
p-1 1
p-1 1
p-0 1
p-0 1
p-0 1
p-1 1
p-0 1
p-1 1
p-1 1
p-0 1
p-0 1
p-0 1
p-0 1
p-0 1
p-0 1
p-0 1
p-1 1
p-1 1
p-0 1
p-0 1
p-0 1
p-0 1
p-1 1
p-0 1
p-1 1
p-1 1
p-0 1
p-0 1
p-0 1
p-1 1
p-1 1
p-0 1
p-1 1

Wegen der eindeutigen Benennung von Transitionen in MUTEX wurde act(t) statt t geschrieben.


  Anfang der Seite


Hierzu ist noch zu bemerken, daß mit Hilfe der Vektoraddition folgende Regeln gelten :

(i) Wenn N schlingenfrei ist, d.h. für kein p Pl und t ->0 gelte
p pre(t) post(t), so gilt

pre(t) M     <=>     M + t 0 .

Bei Schlingen ist folgendes möglich :

t ist nicht bereit in M, aber dennoch gilt M + t = 0.

(ii) Sei jetzt pre(t) M. Dann gilt :

M M'     <=>     M + t = M'

Die transponierte Matrix N' entsteht aus N durch "Kippen um die Hauptdiagonale" :

N' : ->0   ×   Pl ->

wobei

N' (t , p )     =df     N' (p , t ).

Anschaulich sind die Transitionsvektoren jetzt "Zeilen" :


N' p1         . . . .         pm
t1
.

.
.
.

. . .
tn
.



Das Produkt der Matrix N' mit einem Vektor
I : Pl -> ergibt einen Vektor

N' · I : (->0) ->

mit
(N' · I)( t ) = N' (t , p ) · I( p ).


Anschaulich sieht das Produkt N' · I so aus :

N' · I =
t1 · I
. . .
tn · I

Für jede Transition t von N wird also das Skalarprodukt t · I berechnet.

Definition :
Eine S-Invariante von N = ( A, Pl, ->, M0 ) ist ein Vektor

I : Pl -> ,

der das homogene, lineare Gleichungssystem

N' · I = O

löst. Dabei ist O : (->0) -> {0} der passende Nullvektor.


Eigenschaften von S-Invarianten

(i) Mit I1 und I2 ist auch I1 + I2 eine S-Invariante
(ii) Mit I ist auch c · I für c eine S-Invariante
(iii) Mit N' · I = O     <=>     t · I = 0 für alle t ->0


Für das Beispielnetz MUTEX sehen die S-Invarianten als Vektoren wie folgt aus :

MUTEX I1 I2 I3
p1
p2
p3
p4
p5
p6
p7
p-0 1
p-0 1
p-1 1
p-1 1
p-0 1
p-0 1
p-1 1
p-1 1
p-1 1
p-1 1
p-0 1
p-0 1
p-0 1
p-0 1
p-0 1
p-0 1
p-0 1
p-0 1
p-1 1
p-1 1
p-1 1



  Anfang der Seite


Satz :
(Invarianz)
Sei N = ( A, Pl, ->, M0 ) ein Netz. Dann gilt für jede S-Invariante I von N und für jede Markierung mark(N) :

M · I = M0 · I.


Nun zwei anschauliche Deutungen des recht abstrakten Invarianz-Satzes. Zunächst sei hier erläutert, daß M · I = M0 · I ausführlicher

M( p ) · I( p )     =     M0( p ) · I( p )

bedeutet.
(*)


Korollar :
Sei die S-Invariante I die charakteristische Funktion einer Menge Pl0 Pl, d.h. es gelte

I( p ) = 1      falls p Pl0
0      sonst

Dann gilt für alle M mark(N)

M( p )     =     M0( p ).
(**)


Die linke Summe stellt die Tokenanzahl auf den Plätzen in Pl0 unter der Markierung M dar, die rechte Summe die entsprechende Anzahl unter M0.
Anschaulich besagt die Gleichung (**) also :

Die Tokenanzahl auf den Plätzen in Pl0 bleibt invariant.

Für allgemeine S-Invarianten I kann die allgemeine Gleichung (*) wie folgt gelesen werden :

Die gemäß I gewichtete Tokenanzahl bleibt invariant.


Jetzt wird wieder das Beispielnetz MUTEX betrachtet. Mit Hilfe der S-Invarianten wird nun versucht die Eigenschaften (Wechselseitiger Ausschluß und Sicherheit ) nachzuweisen. Die S-Invarianten von N1 sind die bereits beschriebenen Vektoren I1, I2, I3.


(1) Aus I1 folgt mit dem Korollar : Die Tokenanzahl auf { p3, p4, p7 } ist stets 1. Daraus folgt der wechselseitige Ausschluß von p3 und p7 : es liegt niemals gleichzeitig ein Token auf beiden Plätzen.

(2) Zusätzlich liefern I2 und I3 : Auch auf { p1, p2, p3 } und { p5, p6, p7 } ist die Tokenanzahl stets 1. Da jeder Platz von MUTEX in (wenigstens) einer der Mengen

{ p1, p2, p3 }, { p3, p4, p7 }, { p5, p6, p7 }

enthalten ist, folgt daraus die Sicherheit von MUTEX : niemals liegt mehr als ein Token auf einem Platz pi.

(3) Um eine allgemeine S-Invariante kennenzulernen, sei I1 + I2 betrachtet. Dann gilt für alle M mark(N)

M( p1 ) + M( p2 ) + 2 · M( p3 ) + M( p4 ) + M( p7 ) = 2,

d.h. Token auf dem Platz p3 werden doppelt gezäht.


Das Beispiel deutet einen allgemeinen Weg zum Beweis von Netz-Eigenschaften an :


(1) Formulierung der gewünschten Eigenschaften wie "wechselseitiger Ausschluß" oder "Sicherheit" als Eigenschaften der Tokenanzahlen auf gewissen Plätzen.

(2) Analyse : Gewinnung der S-Invarianten aus der Matrizendarstellung des Netzes.

(3) Verifikation : Folgerung der Token-Eigenschaften aus den S-Invarianten.



Vorheriges Kapitel    Nächstes Kapitel


© Copyright Oktober 1997 by Petra Hornstein