6.5.1 Reduktionen des Zustandsgraphen

Zusätzlich zu einer guten Speicherausnutzung bietet INA optional Möglichkeiten, den Zustandsgraphen schon während der Berechnung zu reduzieren. Ziel der Reduktion ist es, geeignete Teilgraphen zu finden, die bestimmte Eigenschaften des Erreichbarkeitsgraphen repräsentieren. Dabei ist es möglich, daß Knoten dieser reduzierten Graphen als Vertreter für ganze Klassen von Knoten des Erreichbarkeitsgraphen stehen, oder daß nur ein Teil der möglichen Zustandsübergänge betrachtet wird und somit einige Bögen und Knoten des Erreichbarkeitsgraphen nicht berechnet werden. Desweiteren gibt es Darstellungen für die unendlichen Zustandsgraphen unbeschränkter Netze.

Als Beispiel für die Zustandsgraphreduktionen dient das Netz 2.2 der speisenden Philosophen. Der Zustandsgraph hat 393 Knoten.

Symmetrische Reduktion

Oftmals treten in einem Netzmodell Symmetrien auf, die bei der Analyse ausgenutzt werden können.

Bei der Berechnung eines Zustands- bzw. Überdeckbarkeitsgraphen, können alle Zustände identifiziert werden, die durch eine Symmetrieabbildung ineinander überführt werden. Die Zahl der zu berechnenden Zuständen wird dadurch unter Umständen erheblich reduziert, so daß die Gesamtberechnung (einschließlich der der Symmetrien) schneller sein kann als die des kompletten Zustandsgraphen. Der Nachteil des symmetrisch reduzierten Zustandsgraphen besteht darin, daß er im allgemeinen nur schwächere Aussagen hinsichtlich der Lebendigkeit von Transitionen liefert.

Die Symmetrien werden entweder separat mit der Funktion <Y> , oder automatisch (falls dies nicht bereits erledigt wurde) vor der Erzeugung eines symmetrisch reduzierten Graphen berechnet. Es werden nur die Generatoren berechnet, aus denen die Symmetrien beim Aufbau des Graphen kombiniert werden können. Im ungüstigen Fall hat ein Netz exponentiell viele Symmetrien, die Anzahl der Generatoren ist aber polynomial in der Netzgröße. Durch die Generierung der Symmetrien aus den zuvor berechneten Generatoren ergibt sich eine enorme Speichereinsparung, dabei hat das implementierte Verfahren im allgemeinen ein gutes Laufzeitverhalten.

<Y> Compute the symmetries of the net

INA berechnet die Symmetriegruppe des aktuellen Netzes unter Berücksichtigung eventueller Zeitbewertungen.

Zuerst müssen Sie angeben, ob Fixpunkte für Plätze oder Transitionen gesetzt oder ob der Anfangszustand als symmetrisch betrachtet werden soll: Do you want to set fixpoints bzw. initial state to be symmetric? Teilweise werden so andere oder gar keine Symmetrien gefunden und die Berechnung abgebrochen: Trivial transition partition bzw. identity is the only symmetry.

Durch Beantwortung der Abfrage Write the symmetries to the session file mit <Y> können Sie die Generatoren der Symmetrien in den Session-Report schreiben lassen, bei <N> werden nur die Zerlegungen der Platz- und Transitionsmengen in Äquivalenzklassen geschrieben.

Während der Berechnung läuft ein Zähler über die gefundenen Generatoren, die laufende Berechnung kann mit <Q> beendet werden.

Am Ende der Berechnung wird die Anzahl der Generatoren und die Anzahl der daraus kombinierbaren Symmetrien ausgegeben.

Die Funktion <Y> kann auch benutzt werden, um eine einmal berechnete Symmetriegruppe erneut berechnen zu lassen. Dazu müssen Sie nur die Frage compute the symmetries once again positiv beantworten. Sie können dabei beispielsweise neue Fixpunkte setzen oder die Anfangsmarkierung berücksichtigen.

Für das Netz 2.1 ohne Vielfachheiten sieht die Berechnung wie folgt aus:

......................Do You want to set fixpoints? Y/N N
.....................Initial state to be symmetric? Y/N Y
..........Write the symmetries to the session file? Y/N Y

Generators:           3

Generating set of the symmetries: 

* Places:      (2 3)(5 6)
  Transitions: (2 3)(5 6)

* Places:      (1 2 3)(4 5 6)
  Transitions: (1 2 3)(4 5 6)

* Places:      (1 3 2)(4 6 5)
  Transitions: (1 3 2)(4 6 5)

3 generators for 6 symmetries found!

Classes of equivalent places:
   1:  4.Prog1_in_Pause,  5.Prog2_in_Pause,  6.Prog3_in_Pause,
   2:  1.Prog1_am_Term,  2.Prog2_am_Term,  3.Prog3_am_Term,
   3:  0.Terminal_frei,

Classes of equivalent transitions:
   1:  4.logout_Prog1,  5.logout_Prog2,  6.logout_Prog3,
   2:  1.login_Prog1,  2.login_Prog2,  3.login_Prog3,

Zuerst wird die Menge der Generatoren in Zyklenschreibweise ausgegeben: Der erste Generator besagt, daß Platz 2 auf Platz 3 und Platz 5 auf Platz 6 abgebildet wird (und umgekehrt), analoges gilt für den ersten Generator bezüglich der Transitionen. Der erste Teil des zweiten Generators besagt, daß Platz 1 auf Platz 2, Platz 2 auf Platz 3 und Platz 3 auf Platz 1 abgebildet wird.

Danach werden die Äquivalenzklassen ausgegeben: Die Plätze 1, 2 und 3 sind zueinander äquivalent, genauso die Plätze 4, 5 und 6. Platz 0 bildet bezüglich der Zerlegung eine Einermenge. Für die Transitionen gilt, daß zum einen 1, 2 und 3, zum anderen 4, 5 und 6 zueinander äquivalent sind.

Abbildung 6.2: Zwei Ampeln (ampel.pnt)

Das Netz 6.2 ist (im Gegensatz zum Netz 2.1) nur ohne Berücksichtigung der Anfangsmarkierung symmetrisch. Es modelliert zwei Ampeln: Die Plätze entsprechen den Farben der beiden Ampeln (es handelt sich aber nicht um ein gefärbtes Netz), die Transitionen sorgen für die notwendige Verkehrssicherheit.

Ein Ablauf der Symmetrieberechnung dieses Netzes kann wie folgt aussehen:

Computing the symmetries
Do You want to set fixpoints? N
Initial state to be symmetric? Y
Identity is the only symmetry!

Compute the symmetries once again? Y
Do You want to set fixpoints? N
Initial state to be symmetric? N

Generating set of the symmetries: 

* Places:      (3 4)
  Transitions: 

* Places:      (1 2)(3 4)(5 6)
  Transitions: (1 3)(2 4)

2 generators for 4 symmetries found!

Classes of equivalent places:
   1:  5.rot_eins,  6.rot_zwei,
   2:  3.gelb_eins,  4.gelb_zwei,
   3:  1.gruen_eins,  2.gruen_zwei,

Classes of equivalent transitions:
   1:  2,  4,
   2:  1,  3,

Da die Philosophen des Netzes 2.2 ein symmetrisches Verhalten haben, lohnt dort die Berechnung der Symmetriegruppe: Der symmetrisch reduzierte Erreichbarkeitsgraph hat nur noch 47 Knoten.

Zu Details siehe [Sta90, Kapitel 7 (62-73)], [Sta91] und [SS91]. Die aktuellste Beschreibung der Implementation findet sich in [Sch97].

Sture Reduktion

Sture Reduktion ist eine weitere Möglichkeit, die Knotenanzahl des Erreichbarkeitsgraphen zu veringern. Sie kann mit der symmetrischen Reduktion kombiniert werden, ist aber nicht für alle Netztypen verfügbar.

Durch eine Freiheit der Reihenfolge des Schaltens von Transitionen, wie sie durch Nebenläufigkeit impliziert wird, kommt es zu einer Erhöhung der Anzahl erreichbarer Zustände. Bei der Untersuchung von zwei Pfaden zu einem Zustand ist eventuell erkennbar, daß diese sich nur in der Reihenfolge unterscheiden, in der unabhängige, d.h. nebenläufige Transitionen geschaltet werden. Der Zustandsgraph enthält alle Zwischenzustände, obwohl diese teilweise redundant sind. Sture Reduktion hat das Ziel, einen möglichst kleinen Ausschnitt aus dem Zustandsgraphen zu konstruieren. In einer gegebenen Markierung wird nur eine Teilmenge von Transitionen geschaltet. Diese Teilmenge wird so gewählt, daß diese von anderen Transitionen möglichst wenig beeinflußt wird, oder nur in bestimmter, vorher bekannter Art. Diese Vorgehensweise beruht wesentlich auf dem Lokalitätsprinzip, sowie auf der Nebenläufigkeit. Bei der Berechnung reicht es im allgemeinen nicht aus, nur die konzessionierten Transitionen zu betrachten, sondern teilweise auch Transitionen ohne Konzession. Die entstehende Menge erhielt aufgrund ihrer schweren Beeinflußbarkeit den Namen sture Menge.

Die wichtigste Eigenschaften, die noch gefolgert werden können, ist die Existenz toter Markierungen und unendlicher Pfade.

Im Netz 2.2 können Philosophen nebenläufig handeln. Der stur reduzierte Erreichbarkeitsgraph hat 183 Knoten. Unter Berücksichtigung der schon zuvor erwähnten Symmetrie des Netzes ergibt sich mit sturer und symmetrischer Reduktion ein Erreichbarkeitsgraph, der sogar nur aus 28 Knoten besteht. Die symmetrische Reduktion ist sozusagen orthogonal zur sturen, es ergibt sich unter Umständen eine insgesamt drastische Reduktion des Zustandsgraphen, beim Beispielnetz 2.2 um den Faktor zehn.

Zu Definitionen und Details der Implementation siehe die Diplomarbeit [Pog94].

Überdeckbarkeitsgrahen

Überdeckbarkeitsgraphen bieten bei unbeschränkten Netzen eine vollständige Übersicht über die Beschränktheit von Plätzen und die Überdeckbarkeit von Markierungen. Ihre Berechnung ist nur für normale Netze ohne Zeitbewertung und Prioritäten unter der normalen Schaltregel möglich und wird daher anderweitig nicht angeboten. INA berechnet den Graphen nach dem Algorithmus von KARP und MILLER. Falls das Netz beschränkt ist, dann entspricht der Überdeckbarkeitsgraph dem normalen Zustandsgraphen.

Zu Details siehe [Sta90, Kapitel 5 (43-53)].

Finkels Methode zur Berechnung des minimalen Überdeckbarkeitsgraphen

FINKEL betrachtet in [Fin89] Erreichbarkeitsgraphen und Überdeckbarkeitsgraphen als Spezialfälle einer allgemeineren Struktur, sogenannter $\omega$-Zustandsgraphen. Unter allen diesen Zustandsgraphen gibt es einen eindeutig bestimmten, der minimal bezüglich Knotenzahl ist. INA bietet für Netze ohne Zeitbewertung und Prioritäten unter der normalen Schaltregel die Möglichkeit, den Überdeckbarkeitsgraphen nach FINKELS Methode zu berechnen und so während des Aufbaus die Knoten- und Kantenzahl zu reduzieren. Für unbeschränkte Netze ergibt sich ein Graph, der weniger Knoten als der klassische Überdeckbarkeitsgraph hat. Für beschränkte Netze bewegt sich der zeitliche Mehraufwand in vertretbaren Grenzen, obwohl keine wirkliche Reduktion erreicht wird. Die Kenntnis des minimalen $\omega$-Zustandsgraphen genügt, um Eigenschaften wie Beschränktheit des Netzes, Überdeckbarkeit von Markierungen oder die Existenz unendlicher Pfade im Erreichbarkeitsgraph zu entscheiden.

Abbildung 6.3: Das alternating bit protocol (altbit.pnt)

Das Netz 6.3 wird gewöhnlich unter der Schrittschaltregel betrachtet und ist dann beschränkt. Wird dieses Netz ohne Schrittschaltregel analysiert, so modelliert es das alternating bit protocol nicht mehr korrekt. Da es dann unbeschränkt ist, wird es hier trotzdem als Beispiel für eine drastische Reduktion des Zustandsgraphen vorgestellt. Die Berechnung des klassischen Überdeckbarkeitsgraphen benötigt mehrere Tage; der Graph hat dann 435316 Knoten. Nach FINKELS Methode ergibt sich ein Graph mit 72 Knoten, die Berechnung dauert nur wenige Sekunden.

Zu Definitionen und Details der Implementation siehe die Diplomarbeit [Lü95].