Zusammenfassung
In order to specify and analyze the behavior of systems (computer programs, circuits etc.) it is important to have a suitable specification language. Although it is possible to define such a language separately for each type of system, it is desirable to have a standard toolbox that allows to do this in a generic way for various – possibly quite different – systems.
Coalgebra, a concept of category theory, has proven to be a suitable framework to model transition systems. This class of systems includes many well-known examples like deterministic automata, nondeterministic automata or probabilistic systems. All these systems are coalgebras and their behavior can be analyzed via the notion of final coalgebra or other category theoretic constructions.
This thesis investigates how to improve and build upon existing results to explore the expressive power of category theory and in particular coalgebra in behavioral analysis. The three main parts of the thesis all have a different focus but are strongly connected by the coalgebraic concepts used.
Part one discusses adjunctions in the context of coalgebras. Here, well-known automata constructions such as the powerset-construction are (re)discovered as liftings of simple and well-known basic adjunctions.
The second part deals with continuous generative probabilistic systems. It is shown that their trace semantics can be captured by a final coalgebra in a category of stochastic relations.
The final contribution is a shift from qualitative to quantitative reasoning. Via the development of methods to lift functors on the category of sets and functions to functors on pseudometric spaces and nonexpansive functions it is possible to define a canonical, coalgebraic framework for behavioral pseudometrics.