A general SOS theory for the specification of probabilistic transition systems

This article focuses on the formalization of the structured operational semantics approach for languages with primitives that introduce probabilistic and non-deterministic behavior. We define a general theoretic framework and present the rule format that guarantees that bisimulation equivalence (in the probabilistic setting) is a congruence for any operator defined in this format. We show that the bisimulation is fully abstract w.r.t. the format and (possibilistic) trace equivalence in the sense that bisimulation is the coarsest congruence included in trace equivalence for any operator definable within the format (in other words, bisimulation is the smallest congruence relation guaranteed by the format). We also provide a conservative extension theorem and show that languages that include primitives for exponentially distributed time behavior (such as IMC and Markov automata based language) fit naturally within our framework.