Structural Operational Semantics for Continuous State Stochastic Transition Systems

In this paper we show how to model syntax and semantics of stochastic processes with continuous states, respectively as algebras and coalgebras of suitable endo-functors over the category of measurable spaces Meas. Moreover, we present an SOS-like rule format, called MGSOS, representing abstract GSOS over Meas, and yielding fully abstract universal semantics, for which behavioral equivalence is a congruence. An MGSOS specification defines how semantics of processes are composed by means of measure terms, which are expressions specifically designed for describing finite measures. The syntax of these measure terms, and their interpretation as measures, are part of the MGSOS specification. We give two example applications, with a simple and neat MGSOS specification: a “quantitative CCS”, and a calculus of processes living in the plane R2 whose communication rate depends on their distance. The approach we follow in these cases can be readily adapted to deal with other quantitative aspects