Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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 ...