Rakow, Astrid (2011) Slicing and reduction techniques for model checking Petri nets. PhD, Universität Oldenburg.

Preview

Volltext (1449Kb)

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.

["eprint_fieldname_abstract_plus" not defined]

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.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	model checking , temporal logics , fairness , Petri net , model reduction
Controlled Keywords:	Model Checking , Temporale Logik , Fairness <Informatik> , Petri-Netz , Ordnungsreduktion
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	17 Jan 2013 14:28
Last Modified:	08 Jul 2013 13:04
URI:	https://oops.uni-oldenburg.de/id/eprint/1332
URN:	urn:nbn:de:gbv:715-oops-14125
DOI:
Nutzungslizenz:

Actions (login required)

View Item