GSOS for probabilistic transition systems
Falk Bartels · Electronic Notes in Theoretical Computer Science · 2002
We introduce probabilistic GSOS, an operator specification format for (reactive) probabilistic transition systems which arises as an adaptation of the known GSOS format for labelled (nondeterministic) transition systems. Like the standard one, The format is well behaved in the sense that on all models bisimilarity is a congruence and the up-to-context proof principle is valid. Moreover, every specification has a final model which can be shown to offer unique solutions for guarded recursive equations. The format covers operator specifications from the literature, so that the well-behavedness results given for those arise as instances of our general one. The novel format was obtained via the following procedure: Turi and Plotkin have modelled specifications in the (standard) GSOS format and their models as natural transformations of a certain shape and a class of bialgebras identified by them. Several well-behavedness results for the concrete format can elegantly be proved in the categorical setting. Since the abstract framework is parametric in the type of system behaviour under consideration, it can be instantiated with that of probabilistic transition systems yielding a specification format for them, again in terms of specific natural transformations. The main contribution of this paper is the derivation of probabilistic GSOS as a rule-style representation of those.