10.18453/rosdok_id00003271 Liebke, Torsten Torsten Liebke http://d-nb.info/gnd/1243527919 Universität Rostock 2020 004 Data processing Computer sciences 2020 en http://purl.uni-rostock.de/rosdok/id00003271 urn:nbn:de:gbv:28-rosdok_id00003271-3 Model checking is the automated verification that systematically checks if a given behavioral property holds for a given model of a system. We use Petri nets and temporal logic as formalisms to describe a system and its behavior in a mathematically precise and unambiguous manner. The contributions of this thesis are concerned with the improvement of model checking efficiency both in theory and in practice. We present two new reduction techniques and several supplementary strength reduction techniques. The thesis also enhances partial order reduction for certain temporal logic classes.