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.
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.
INA berechnet die Symmetriegruppe des aktuellen Netzes unter Berücksichtigung eventueller Zeitbewertungen.Zuerst müssen Sie angeben, ob der Anfangszustand als symmetrisch betrachtet oder ob Fixpunkte für Plätze oder Transitionen gesetzt werden sollen: Initial state to be symmetric bzw. do you want to set fixpoints? Teilweise werden so andere oder gar keine Symmetrien gefunden und die Berechnung abgebrochen: Identity is the only symmetry. Falls dagegen Symmetrien gefunden wurden, so können Sie diese mit Write the symmetries to the session file in den Session-Report schreiben, andernfalls werden nur die Äquivalenzklassen geschrieben.
Sollte in einem Teil der Berechnung ein Speicherüberlauf vorkommen, so meldet INA : Stopped by heap overflow danger. Die Untersuchung kann abbrechen, weil es mehr Symmetrien gibt, als der Speicher fassen kann: Sorry, no space for computation. Die Berechnung kann aber auch mit <Q> beendet werden, wenn Sie glauben, über eine hinreichend große Untergruppe der Symmetriegruppe zu verfügen. INA rechnet auf jeden Fall solange, bis eine vollständige Untergruppe berechnet ist.
Bei der Ausgabe der Symmetrien können Sie erkennen, wie die Zeilen berechnet wurden: Einträge, die mit einem Stern (*) versehen sind, sind durch Verkettung aus den Generatoren (Einträge ohne *) entstanden. Die erste Zeile entspricht immer der Identität.
Neben den Symmetrien werden die Zerlegungen der Platz- und Transitionsmengen in Äquivalenzklassen berechnet.
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 sieht die Berechnung wie folgt aus:
Computation of the symmetries:
1: 0 1 2 3 4 5 6 * 1 2 3 4 5 6
2: 0 1 3 2 4 6 5 * 1 3 2 4 6 5
3: 0 2 1 3 5 4 6 * 2 1 3 5 4 6
* 4: 0 2 3 1 5 6 4 * 2 3 1 5 6 4
* 5: 0 3 1 2 6 4 5 * 3 1 2 6 4 5
* 6: 0 3 2 1 6 5 4 * 3 2 1 6 5 4
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 Symmetriegruppe aufgeführt, dann die Äquivalenzklassen: 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.1: Zwei Ampeln (ampel.pnt)
Das Netz 6.1 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
Initial state to be symmetric? Y
Do You want to set fixpoints? N
Identity is the only symmetry!
Compute the symmetries once again? Y
Initial state to be symmetric? N
Do You want to set fixpoints? N
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 47 Knoten.
Zu Details siehe [Sta90, Kapitel 7 (62-73),], [Sta91] und [SS91].
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].
Ü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),].
FINKEL betrachtet in [Fin89] Erreichbarkeitsgraphen und
Überdeckbarkeitsgraphen als Spezialfälle einer allgemeineren Struktur,
sogenannter 
-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 -Zustandsgraphen genügt, um
Eigenschaften wie Beschränktheit des Netzes, Überdeckbarkeit von
Markierungen oder die Existenz unendlicher Pfade im Erreichbarkeitsgraph
zu entscheiden.
Abbildung 6.2: Das alternating bit protocol (altbit.pnt)
Das Netz 6.2 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].
Zuletzt geändert am: Thu Apr 10 15:08:18 MET DST 1997