An Exercise on Transition Systems

Labelled transition systems admit different but equivalent characterizations either as relational structures or coalgebras for the powerset functor, each of them with their own merits. Notions of simulation and bisimulation, for example, are expressed in the pointfree relational calculus in a very concise and precise way. On the other hand, the coalgebraic perspective regards processes as inhabitants of a final universe and allows for an intuitive definition of the semantics of process' combinators.This paper is an exercise on such a dual characterisation. In particular, it discusses how a notion of weak bisimilarity can be lifted from the relational to the coalgebraic level, to become an effective reasoning tool on coinductively defined process algebras.