Abstract in Englisch:

Lattice theory is a well studied area of mathematics and finds many applications, for example in system verification. By Knaster-Tarksi, any monotone function f∶L → L on a complete lattice L admits a least and a greatest fixpoint. It often occurs that one is specifically interested in such a least or greatest fixpoint. This thesis provides a framework which can be used to verify if some fixpoint a ∈ L of f is indeed the least/greatest fixpoint of f. Additionally, we are able to derive lower/upper bounds for least/greatest fixpoints. This theory will be embedded into a (gs-)categorical framework which allows us to create a tool for fixpoint verification. Additionally, there is interest in computing these least/greatest fixpoints as no general method exists which always yields an exact computation. To this end, we provide a generalization of strategy iteration which allows one to compute least/greatest fixpoints. Throughout this thesis we provide a wide range of applications where these methods can be applied. These include a variety of state-based system - termination probability of Markov chains, bisimilarity for transition systems and behavioural metrics for labeled Markov chains, metric transition systems and probabilistic automata - and three two-player-games - discounted mean-payoff games, simple stochastic games and energy games.