{"id":{"repo_id":"oldenburg","oai_identifier":"oai:oops.uni-oldenburg.de:1332"},"canonical_url":"https://search.dev.ndltd.org/etd/oldenburg/oai:oops.uni-oldenburg.de:1332","repository":{"repo_id":"oldenburg","name":"Carl von Ossietzky Universität Oldenburg","base_url":"http://oops.uni-oldenburg.de/cgi/oai2"},"display":{"title":"Slicing and reduction techniques for model checking Petri nets","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Rakow, Astrid"],"institution":"Universität Oldenburg","degree_name":null,"degree_level":"thesis.doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-07-08","date_published":"2011-07-08","updated_at":"2026-07-27T20:28:09Z","subjects":["model checking , temporal logics , fairness , Petri net , model reduction"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://oops.uni-oldenburg.de/1332","outbound_label":"Repository record","outbound_source":"source_url"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Rakow, Astrid"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:publisher","label":"Institution","values":["BIS der Universität Oldenburg"]},{"key":"dc:type","label":"Dc Type","values":["doctoralThesis"]},{"key":"thesis:degree_level","label":"Degree Level","values":["thesis.doctoral"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Universität Oldenburg"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["model checking , temporal logics , fairness , Petri net , model reduction"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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.","In this work we develop two Petri net reduction approaches, Petri net slicing and cutvertex reductions, to tackle the state space explosion problem for model checking. Petri net reductions are transformations of the Petri net that decrease its size. As a mean against the state space explosion problem for model checking they have to preserve temporal properties and reduce its state space. Petri net reductions can conveniently be daisy chained with other methods fighting state space explosion. For a given net N and temporal logic formula f, both approaches determine a net N' that contains at least scp(f), the set of the Petri net places f refers to, and simplifies the remaining net such that N' is equivalent with respect to f. To preserve liveness properties, we show that it suffices to assume a form of weak fairness, which we call relative fairness. We consider the temporal logic CTL* and its sublogics."]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Slicing and reduction techniques for model checking Petri nets"]}]}],"canonical_facts":{"dc:creator":["Rakow, Astrid"],"dc:description.abstract":["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.","In this work we develop two Petri net reduction approaches, Petri net slicing and cutvertex reductions, to tackle the state space explosion problem for model checking. Petri net reductions are transformations of the Petri net that decrease its size. As a mean against the state space explosion problem for model checking they have to preserve temporal properties and reduce its state space. Petri net reductions can conveniently be daisy chained with other methods fighting state space explosion. For a given net N and temporal logic formula f, both approaches determine a net N' that contains at least scp(f), the set of the Petri net places f refers to, and simplifies the remaining net such that N' is equivalent with respect to f. To preserve liveness properties, we show that it suffices to assume a form of weak fairness, which we call relative fairness. We consider the temporal logic CTL* and its sublogics."],"dc:format.medium":["application/pdf"],"dc:publisher":["BIS der Universität Oldenburg"],"dc:subject":["model checking , temporal logics , fairness , Petri net , model reduction"],"dc:title":["Slicing and reduction techniques for model checking Petri nets"],"dc:type":["doctoralThesis"],"thesis:degree_level":["thesis.doctoral"],"thesis:institution_name":["Universität Oldenburg"]},"updated_at":"2026-07-27T20:28:09Z"}