Algorithms and Hardness Results for Object Nets

Abstract

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.