In the setting of (nondeterministic) labeled transition systems, Turi and Plotkin [1] found that GSOS rules essentially correspond to natural transformations of a certain type, which they call abstract GSOS. Those in turn correspond to distributive laws of a monad over a copointed functor as Lenisa, Power, and Watanabe [2] explain.

In previous work we have shown that the operators defined by this type of specification are well behaved in the sense that

guarded recursive equations involving them have unique solutions and that

they yield a valid bisimulation up-to-context technique.

In this talk we consider transition systems involving both, nondeterminism and probability, and introduce an SOS-style specification format for them. To prove that the format is well behaved, it is shown that it is related to the corresponding instance of abstract GSOS. [1]

D. Turi and G Plotkin, Towards a mathematical operational semantics, LICS'97 [2]

M. Lenisa, J. Power, and H. Watanabe, Distributivity for endofunctors, pointed and copointed endofunctors, monads and comonads, CMCS 2000