Petri-Netze

Motivation

Als Aktivitätsdiagramme (activity diagrams) in UML.

Modellierung von nebenläufigen (concurrent/parallel) Systemen.

  • Automat mit mehreren aktiven Stellen

Endliche Automaten ungeeignet:

  • Anzahl der Zustände steigt exponentiell
  • Nur jeweils ein aktiver Zustand

Definition

Marken / Tokens Aktive Stelle, dürfen nur gleichzeitig weiter

Stellen / Places Plätze für Marken

Transitionen "feuern" wenn alle Eingangszustände Marken besitzen. (Synchronisation)

Marken werden dann konsumiert und neu erzeugt.

Es darf eine beliebige Transition gewählt werden.

Formale Definition

N=⟨S,T,∙(),()∙,m0⟩ N=\left\langle S, ~T,~^\bullet(),~()^{\bullet},~ m_{0}\right\rangle 

SS Stellen-Menge

TT Transitions-Menge

∙():T↦M^\bullet(): T\mapsto M Vorbedingungen (von Transition)

()∙:T↦M()^\bullet:T\mapsto M Nachbedingungen (von Transition)

M…M \dots Markierungs-Zähler-Menge

Alle Funktionen die Marken von jeder Stelle zählen: S↦NS\mapsto \N

Teilmengen: (sind Mengen obwohl klein geschrieben)

m0∈Mm_{0} \in M Anzahl der Marken an jeder Stelle zu Beginn

∙t∈M^\bullet t \in M Anzahl der entfernten Marken von jeder Stelle durch Transition tt

t∙∈Mt^\bullet \in M Anzahl der hinzugefügten Marken von jeder Stelle durch Transition tt

Beliebige m,m′,m′′∈Mm, m',m'' \in M :

∀s∈S:\forall s\in S:

Ordnung m≤m′m \leq m'fallsm(s)≤m′(s)m(s) \leq m^{\prime}(s)

Addition m⊕m′=m′′m \oplus m^{\prime}=m^{\prime \prime}fallsm(s)+m′(s)=m′′(s)m(s)+m^{\prime}(s) = m^{\prime \prime}(s)

Subtraktion m⊖m′=m′′m \ominus m^{\prime}=m^{\prime \prime}fallsm(s)−m′(s)=m′′(s)m(s)-m^{\prime}(s) = m^{\prime \prime}(s)

Schalten und Erreichbarkeit

tt Transition

mm Anzahl der Marken an jeder Stelle die mit Transition verbunden ist

ttist fürmmaktiviert wenn∙t≤m^\bullet t \leq m

Anzahl der entfernten Marken von jeder Stelless durch Transition tt ≤ Anzahl der Marken in jeder Stelle aus mm

∙t(S1)≤m(S1)^\bullet t(S_1) \leq m(S_1)

∙t(S2)≤m(S2)^\bullet t(S_2) \leq m(S_2)

…\dots

∙t(Sn)≤m(Sn)^\bullet t(S_n) \leq m(S_n)

wenn an jeder Stelle SiS_i genug Marken vorhanden sind, um die Transition zu schalten.

Wennttschaltet / feuert nachdem es vonmmaktiviert wurde, dann

m′=m⊖∙t⊕t∙m^{\prime}=m ~\ominus~^{\bullet} t ~\oplus ~ t^{\bullet}

Werden die Tokens die ∙t^\bullet t verlangt hat von mm abgezogen und die Tokens die t∙t^\bullet generiert dem mm hinzugefügt.

Das machen die Funktionen:

∙():T↦M^\bullet(): T\mapsto M Vorbedingungen (von Transition)

()∙:T↦M()^\bullet:T\mapsto M Nachbedingungen (von Transition)

Symbolische Abkürzung dafür:

m[t⟩m′m[t\rangle m^{\prime}

Eine Markierungmnm_n(Funktion nur für einer einzigen StelleSiS_i) ist "erreichbar im Netz" wenn,

es eine Folge von Transitionen t1,…,tnt_{1}, \ldots, t_{n} gibt sodass m0[t1⟩m1…mn−1[tn⟩mn m_{0}\left[t_{1}\right\rangle m_{1} \ldots m_{n-1}\left[t_{n}\right\rangle m_{n} 

(wobei m0m_0 die Anfangsmarkierung ist).

Graphische Notation

für ∙t,t∙^\bullet t, t^\bullet zwischen ss und tt

Kein Pfeil ∙t(s)=0( bzw. t∙(s)=0) { }^{\bullet} t(s)=0\left(\text { bzw. } t^{\bullet}(s)=0\right) 

Ein Pfeil ∙t(s)=1( bzw. t∙(s)=1) { }^{\bullet} t(s)=1\left(\text { bzw. } t^{\bullet}(s)=1\right) 

Ein Pfeil mit Beschriftung ∙t(s)=n>1, (bzw. t∙(s)=n>1) { }^{\bullet} t(s)=n>1, \text { (bzw. } \left.t^{\bullet}(s)=n>1\right) 

∙t(s),t∙(s)^\bullet t(s), t^{\bullet}(s) wird auch als Gewicht bezeichnet.

Modellierungs-Beispiele

Ampel
Dining Philosophers
Leser-Schreiber-Problem
Hermann-Lin
hermann_lin_marked_(1).pdf