Slicing and reduction techniques for model checking Petri nets

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.

Level thesis:degree_level

thesis.doctoral

Grantor dc:publisher

Universität Oldenburg

Year

2011

Author dc:creator

• Rakow, Astrid

• model checking , temporal logics , fairness , Petri net , model reduction

Repository record source_url

http://oops.uni-oldenburg.de/1332

OAI identifier oai:identifier

oai:oops.uni-oldenburg.de:1332