Relation Liftings in Coalgebraic Modal Logic
Johannes Marti
Abstract:
In this thesis we study relation liftings in the context of
coalgebraic modal logic. In the first part of the thesis we look for
conditions on relation liftings that can be used to define a notion of
bisimilarity between states in coalgebras, such that two states are
bisimilar if and only if they are behaviorally equivalent. We show
that this is the case for relation liftings that are lax extensions
and additionally preserve diagonal relations. In the second part of
the thesis we develop a coalgebraic nabla logic for an arbitrary lax
extension. For this logic we prove that, under additional conditions,
bisimulation quantifiers are definable in the nabla logic. This has a
Uniform Interpolation Theorem as consequence.