The talk will be about a recently finished paper of the same name (obtainable via my homepage at http://www.cwi.nl/~bartels).

Transition systems are often specified by operational rules in GSOS format, the models of which are known to be well behaved in many respects. Turi and Plotkin have shown a close relation between such rule sets and their models on the one hand and natural transformations of a certain shape and a class of bialgebras they identify on the other hand. Since the latter formulation generalizes the format to arbitrary types of systems, they called it abstract GSOS. It turns out that several properties of the models can be shown in the abstract setting already. In addition to being more elegant, these proofs have the advantage of covering behaviours different from that of (nondeterministic) labelled transitions systems.

To substantiate this point, we turn to (reactive) probabilistic transition systems. A powerful (concrete) rule format for them is introduced which gives rise to specifications in the corresponding instance of abstract GSOS. From this one can conclude that their models are well behaved in the sense that e.g. the greatest bisimulation is a congruence for their operators and that they make bisimulation up-to-context a valid proof principle for bisimilarity.