×VerfasserIn
	1243527919

Torsten Liebke

Improving explicit model checking for Petri nets

Universität Rostock, 2020

https://doi.org/10.18453/rosdok_id00003271

Abstract: 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.

Dissertation   Freier Zugang