Erreichbarkeitsgraph
Ein Erreichbarkeitsgraph (auch Markierungsgraph genannt) ist ein gerichteter Graph, der aus einem Petri-Netz und einer Anfangsmarkierung gewonnen werden kann. Er wird dadurch erzeugt, dass, mit der Anfangsmarkierung beginnend, die Menge der in der Markierung aktivierten Transitionen ermittelt und jeweils die Folgemarkierung berechnet wird. Die Markierungen werden durch Knoten im Erreichbarkeitsgraphen dargestellt und der Übergang einer Markierung zu ihrer Folgemarkierung wird als Kante im Graphen vermerkt. Für jede Folgemarkierung wird dieser Vorgang wiederholt.
Formale Definition
BearbeitenDer Erreichbarkeitsgraph eines Netzes ist als definiert, wobei die Menge der Knoten, die Menge der Markierungen der Knoten und die Menge der gerichteten Kanten des Graphen ist.
E besteht aus Tripeln , wobei m eine von der Anfangsmarkierung aus erreichbare Markierung ist, von der durch Schalten der Transition t nach m' gelangt werden kann. Jeder Knoten des Erreichbarkeitsgraphen ist eine Markierung Mi der Knotenmenge V des Netzes. Ein Pfad des Markierungsgraphen entsteht durch die Änderung der Markierung, also eine Umbelegung der Marken an V. Der komplette Graph zeigt die Übergänge von jedem Mi zu Mi+1 durch E(Mi,t,Mi+1).
Algorithmus zur Erzeugung des Erreichbarkeitsgraphen
BearbeitenDer folgende Algorithmus in Pseudocode erzeugt den Erreichbarkeitsgraphen eines Netzes und der Anfangsmarkierung
function create_reachability_graph(N, m0) V := {} E := {} pending = {m0} while pending is not empty choose m from pending pending := pending \ {m} if m not in V V := V {m} foreach transition t activated in m do calculate m' such that E := E {(m, t, m')} pending := pending {m'}
Analyse von Erreichbarkeitsgraphen
BearbeitenMit Hilfe von Erreichbarkeitsgraphen lassen sich Petri-Netze analysieren. Beispielsweise lässt sich anhand des Erreichbarkeitsgraphen erkennen, ob ein Netz mit einer gegebenen Anfangsmarkierung lebendig ist. Ebenfalls lässt sich die Reversibilität des Netzes nachweisen oder widerlegen.
Beispiel
BearbeitenBetrachtet sei das folgende ungefärbte Petri-Netz PN mit der Anfangsmarkierung 2p1 + p2.
In der Anfangsmarkierung sind die Transitionen t1, t2 und t3 aktiviert.
1. Iteration
V = {2p1+p2, p1+2p2, 2p1+p3}
E = {(2p1+p2, t1, p1+2p2), (2p1+p2, t2, 2p1+p3), (2p1+p2, t3, 2p1+p3)}
2. Iteration
V = {2p1+p2, p1+2p2, 2p1+p3, 3p2, p1+p2+p3}
E = {(2p1+p2, t1, p1+2p2), (2p1+p2, t2, 2p1+p3), (2p1+p2, t3, 2p1+p3), (p1+2p2, t1, 3p2), (p1+2p2, t2, p1+p2+p3), (p1+2p2, t3, p1+p2+p3), (2p1+p3, t1, p1+p2+p3)}
3. Iteration
V = {2p1+p2, p1+2p2, 2p1+p3, 3p2, p1+p2+p3, 2p2+p3, p1+2p3}
E = {(2p1+p2, t1, p1+2p2), (2p1+p2, t2, 2p1+p3), (2p1+p2, t3, 2p1+p3), (p1+2p2, t1, 3p2), (p1+2p2, t2, p1+p2+p3), (p1+2p2, t3, p1+p2+p3), (2p1+p3, t1, p1+p2+p3), (3p2, t2, 2p2+p3), (3p2, t3, 2p2+p3), (p1+p2+p3, t1, 2p2+p3), (p1+p2+p3, t2, p1+2p3), (p1+p2+p3, t3, p1+2p3)}
4. Iteration
V = {2p1+p2, p1+2p2, 2p1+p3, 3p2, p1+p2+p3, 2p2+p3, p1+2p3, p2+2p3}
E = {(2p1+p2, t1, p1+2p2), (2p1+p2, t2, 2p1+p3), (2p1+p2, t3, 2p1+p3), (p1+2p2, t1, 3p2), (p1+2p2, t2, p1+p2+p3), (p1+2p2, t3, p1+p2+p3), (2p1+p3, t1, p1+p2+p3), (3p2, t2, 2p2+p3), (3p2, t3, 2p2+p3), (p1+p2+p3, t1, 2p2+p3), (p1+p2+p3, t2, p1+2p3), (p1+p2+p3, t3, p1+2p3), (2p2+p3, t2, p2+2p3), (2p2+p3, t3, p2+2p3), (p1+2p3, t1, p2+2p3)}
5. Iteration
V = {2p1+p2, p1+2p2, 2p1+p3, 3p2, p1+p2+p3, 2p2+p3, p1+2p3, p2+2p3, 3p3}
E = {(2p1+p2, t1, p1+2p2), (2p1+p2, t2, 2p1+p3), (2p1+p2, t3, 2p1+p3), (p1+2p2, t1, 3p2), (p1+2p2, t2, p1+p2+p3), (p1+2p2, t3, p1+p2+p3), (2p1+p3, t1, p1+p2+p3), (3p2, t2, 2p2+p3), (3p2, t3, 2p2+p3), (p1+p2+p3, t1, 2p2+p3), (p1+p2+p3, t2, p1+2p3), (p1+p2+p3, t3, p1+2p3), (2p2+p3, t2, p2+2p3), (2p2+p3, t3, p2+2p3), (p1+2p3, t1, p2+2p3), (p2+2p3, t2 3p3), (p2+2p3, t3, 3p3)}
In der letzten Markierung 3p3 ist keine Transition mehr aktiviert.
Grenzen bei der Erzeugung von Erreichbarkeitsgraphen
BearbeitenErreichbarkeitsgraphen lassen sich nur für beschränkte Netze vollständig berechnen. Für unbeschränkte Netze würde der Erreichbarkeitsgraph unendlich groß werden. In solchen Fällen werden häufig Überdeckungsgraphen konstruiert. Zwar lassen Überdeckungsgraphen in vielen Fällen keine Aussagen über die Reversibilität des Netzes zu, aber mit ihnen lassen sich andere Aspekte, wie zum Beispiel die Unbeschränktheit von Stellen, formal betrachten.