FAQ
© 2015 Staats- und Universitätsbibliothek
Hamburg, Carl von Ossietzky

Öffnungszeiten heute09.00 bis 24.00 Uhr alle Öffnungszeiten

Eingang zum Volltext in OPUS

Hinweis zum Urheberrecht

Dissertation zugänglich unter
URN: urn:nbn:de:gbv:18-63649
URL: http://ediss.sub.uni-hamburg.de/volltexte/2013/6364/


Algorithms and Hardness Results for Object Nets

Algorithmen und Komplexitätsresultate für Objektnetze

Heitmann, Frank Andreas

pdf-Format:
 Dokument 1.pdf (1.631 KB) 


SWD-Schlagwörter: Beschränkung , Erreichbarkeit , Algorithmus , Komplexität
Freie Schlagwörter (Deutsch): Objektpetrinetz
Freie Schlagwörter (Englisch): Object-Petri-Net , Restriction , Reachability , Algorithm , Complexity
Basisklassifikation: 54.10
Institut: Informatik
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Hauptberichter: Köhler-Bußmeier, Michael (Vertr.-Prof. PD Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 03.07.2013
Erstellungsjahr: 2013
Publikationsdatum: 29.08.2013
Kurzfassung auf Englisch: The central question tackled in this thesis is, how the formalism of elementary
object systems can be restricted, such that it retains most of its modelling
features, but the verification of properties of the net system becomes feasible.

Elementary object systems are a Petri net formalism introduced by Valk. In
elementary object systems the tokens of a usual Petri net are allowed to have
an inner activity. To this end, these tokens are again modelled by Petri nets
and thus a two levelled structure arises. This formalism and similar formalisms
where Petri nets are somehow nested are helpful for the modelling of applications
where the mobility of entities and the interaction between them are of importance.

The ability to solve important verification problems automatically and efficiently
makes such a formalism far more attractive for practical purposes.
However, being Turing-complete, elementary object systems need to be restricted
if algorithmic solutions to important verification problems ought to be found.

In this thesis, several structural and dynamic restrictions of the formalism
are introduced. The focus is then on the complexity of the reachability problem
as one of the most prominent verification problems. Evident in the severe complexity
bounds we establish even for structurally heavily restricted formalisms is that
these restrictions alone are not enough to solve the reachability problem quickly.
For elementary object systems with a safeness constrain we then show that not
only reachability but every property expressible in the temporal logics
LTL or CTL can be decided in polynomial space. This result holds without any
further structural restrictions and we even show that such further restrictions
have little to no effect. We also argue that other safeness constrains are too
weak to establish a similar result.

Diverging from the central question, we also enhance the formalism of elementary
object systems to object net systems. These allow the vertical transport of tokens
and thus the nesting depth might change. We use these to introduce elementary
object systems with an arbitrarily but fixed nesting depth and show that for these
a similar safeness definition as for elementary object systems can be introduced.
For these and for object net systems with a stronger safeness notion we establish
a similar result as above, namely that LTL and CTL model checking is possible in
polynomial space.

Safe elementary object systems and strongly safe object nets thus are formalisms,
which allow to model mobility and interaction, but which also allow the automatic
verification of properties, using an affordable amount of resources.
Kurzfassung auf Deutsch: Im Zentrum dieser Arbeit steht die Frage, wie der Formalismus der elementaren
Objektsysteme so eingeschränkt werden kann, dass die Möglichkeiten der
Modellierung weitestgehend erhalten bleiben, Eigenschaften des Objektsystems
aber automatisch und effizient überprüft werden können.

Elementare Objektsysteme sind Petrinetze, deren Marken eine innere Aktivität
haben können und dazu selbst wieder als Petrinetz modelliert werden. Das
entstehende Netzsystem hat dann eine zweistufige Struktur. Dieser von Valk
eingeführte Formalismus und ähnliche Formalismen sind bei der Modellierung
von Anwendungen nützlich, bei denen die Mobilität von Objekten und die
Interaktionen zwischen diesen Objekten von Bedeutung sind.

Die Attraktivität eines solchen Formalismus wird durch die Möglichkeit, wichtige
Verifikationsprobleme effizient lösen zu können, stark gesteigert. Da elementare
Objektsysteme allerdings Turing-vollständig sind, muss der Formalismus
eingeschränkt werden, wenn wichtige Probleme einer algorithmischen Lösung
zugänglich sein sollen.

In dieser Arbeit werden zahlreiche strukturell und dynamisch eingeschränkte
Varianten des Formalismus eingeführt und untersucht. Der Fokus liegt dabei
auf der Komplexität des Erreichbarkeitsproblems, einem der wichtigsten
Verifikationsprobleme. Durch die hohen unteren Schranken, die selbst für
strukturell stark eingeschränkte Formalismen bewiesen werden können, wird
deutlich, dass strukturelle Einschränkungen alleine nicht genügen, soll das
Erreichbarkeitsproblem effizient gelöst werden. Für elementare Objektsysteme
wird dann ein Sicherheitsbegriff eingeführt. Für sichere elementare Objektsysteme
kann dann nicht nur das Erreichbarkeitsproblem, sondern jede Eigenschaft, die
in den temporalen Logiken LTL oder CTL ausgedrückt werden kann, in polynomialen
Platz entschieden werden. Dies gilt ohne weitere strukturelle Einschränkungen und
tatsächlich haben diese nun kaum noch einen Effekt. Des weiteren kann für einen
schwächeren Sicherheitsbegriff kein entsprechendes Resultat gezeigt werden.

Abweichend von der zentralen Fragestellung dieser Arbeit wird zuletzt
der Formalismus der elementaren Objektsysteme erweitert. Objektnetzsysteme
erlauben den vertikalen Transport von Marken, wodurch sich die Verschachtelungstiefe
ändern kann. Des weiteren werden elementare Objektsysteme mit einer beliebigen,
aber festen Verschachtelungstiefe eingeführt. Mit einem ähnlichen Sicherheitsbegriff
wie zuvor kann für diese und für Objektnetzsysteme mit einem stärkeren Sicherheitsbegriff
erneut bewiesen werden, dass das Problem der Modellprüfung für LTL und CTL in
polynomialen Platz entschieden werden kann.

Sichere elementare Objektsysteme und stark sichere Objektnetzsysteme sind
somit Formalismen, die es ermöglichen, Mobilität und Interaktionen zu modellieren,
die es aber zugleich auch erlauben, wichtige Eigenschaften automatisch und mit
einem vertretbaren Aufwand zu überprüfen.

Zugriffsstatistik

keine Statistikdaten vorhanden
Legende