Volltextdatei(en) vorhanden
Titel: Algorithms and Hardness Results for Object Nets
Sonstige Titel: Algorithmen und Komplexitätsresultate für Objektnetze
Sprache: Englisch
Autor/Autorin: Heitmann, Frank Andreas
Schlagwörter: Objektpetrinetz; Object-Petri-Net; Restriction; Reachability; Algorithm; Complexity
GND-Schlagwörter: Beschränkung; Erreichbarkeit; Algorithmus; Komplexität
Erscheinungsdatum: 2013
Tag der mündlichen Prüfung: 2013-07-03
Zusammenfassung: 
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.

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.
URI: https://ediss.sub.uni-hamburg.de/handle/ediss/5074
URN: urn:nbn:de:gbv:18-63649
Dokumenttyp: Dissertation
Hauptberichter: Köhler-Bußmeier, Michael (Vertr.-Prof. PD Dr.)
Enthalten in den Sammlungen:Elektronische Dissertationen und Habilitationen

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat  
Dissertation.pdf1.63 MBAdobe PDFÖffnen/Anzeigen
Zur Langanzeige

Diese Publikation steht in elektronischer Form im Internet bereit und kann gelesen werden. Über den freien Zugang hinaus wurden durch die Urheberin / den Urheber keine weiteren Rechte eingeräumt. Nutzungshandlungen (wie zum Beispiel der Download, das Bearbeiten, das Weiterverbreiten) sind daher nur im Rahmen der gesetzlichen Erlaubnisse des Urheberrechtsgesetzes (UrhG) erlaubt. Dies gilt für die Publikation sowie für ihre einzelnen Bestandteile, soweit nichts Anderes ausgewiesen ist.

Info

Seitenansichten

33
Letzte Woche
Letzten Monat
geprüft am 27.11.2020

Download(s)

1
Letzte Woche
Letzten Monat
geprüft am 27.11.2020
Werkzeuge

Google ScholarTM

Prüfe