Sture Transitionen

Zusammenfassung

Im Abschnitt 7 haben wir Erreichbarkeitsgraphen betrachtet, die nicht alle erreichbaren Markierungen enthalten, es aber dennoch gestatten, Aussagen über das Verhalten des betreffenden Netzes abzuleiten. Die Hauptschwierigkeit des angegebenen Verfahrens besteht in der Bestimmung der Symmetriegruppe des Netzes bzw. einer adäquaten Untergruppe. Ist ein Netz graphisch gegeben, so kann es leicht sein, (wie in unseren Beispielen) wenigstens einige Symmetrien visuell zu erkennen. Wir müssen aber auch ari Anwendungsfälle denken, wie sie bei der Verifikation von Kommunikationssoftware auftreten, wo das Netz aus einer irgendwie gegebenen Spezifikation automatisch erzeugt wird. Der hier dargestellte Ansatz von VALMARI vermeidet diese Schwierigkeit, er nutzt stattdessen Freiheiten in der Reihenfolge des Schaltens von Transitionen aus, wie sie von Nebenläufigkeit (vgl. Abschnitt 3) impliziert werden. Das Ziel besteht auch hier darin, einen möglichst kleinen Ausschnitt des Erreichbarkeitsgraphen zu konstruieren, aus dem sich noch Aussagen beweisen lassen. Der zentrale Begriff dabei ist der der sturen Menge von Transitionen.