Verification should be a major building block in any complex development process.
In general, software systems grow over the years and become almost unmanageable over time. Therefore, theoretical modelling and verification techniques have become an integral part in the computer science community.
In the last decades, the question whether an implementation meets the specification serves as motivation to focus on model checking or logical equivalence where requirements are formulated via logical formulas.
In order to enable these verification methods, state-based systems and notions of
behavioural equivalence or distance provide suitable models and techniques to analyze and verify program code. At this point, coalgebra – a concept of category theory –enters the scene. Coalgebra enables the modelling of different state-based systems including branching types such as non-determinism, determinism, or probabilistic systems. Furthermore, the coalgebraic framework provides an abstract definition of modalities which are used to construct formulas. Therefore, the study of verification problems from a coalgebraic (i.e. abstract) point of view enables the development of generic algorithms.
Another focus in this thesis is given in terms of games which provide alternative semantics with respect to behavioural notions such as bisimulation or language
equivalence or in terms of model checking.
Therefore, this dissertation aims at contributing to the research area of logic and
games via generic frameworks given by category theory or lattice theory.