| Popis: |
In der vorliegenden Arbeit werden zwei Reduktionsansätze für Petri-Netze vorgestellt, Petri-Netz Slicing und Cutvertex Reduktionen. Beide Ansätze zielen darauf ab, der Zustandsraumexplosion beim Model Checken entgegenzuwirken. Dazu transformieren sie ein gegebenes Petri-Netz in ein kleineres Netz, so dass gleichzeitig die untersuchte Eigenschaft bewahrt wird. Da Petri-Netz-Reduktionen das Modell transformieren, können sie leicht mit anderen Methoden kombiniert werden. Für ein gegebenes Netz N und eine temporal-logische Eigenschaft f bestimmen beide Ansätze ein Netz N', das wenigstens scp(f), die Menge der Petri-Netzstellen auf die sich f bezieht, enthält, und vereinfachen das übrige Netz so, dass N' in Bezug auf f äquivalent zu N ist. Wir zeigen, dass es genügt, eine schwache Form von Fairness anzunehmen, die wir relative Fairness nennen, um Lebendigkeitseigenschaften zu erhalten. Als temporale Logik untersuchen wir CTL* und ihre Teillogiken. |
