Semantics, bisimulation and congruence results for a general stochastic process operator

We introduce a general stochastic process operator $\frac{f}{d:~D} p(d)$ which behaves as the process $p(d)$ where the value $d$ is chosen from a data domain $D$ with a probability density determined by $f$. We require that $f$ is a measurable function from $D$ to $\mathbb{R}^{\geq 0}$ such that $\int_{d \in D} f(d)d\mu_D = 1$. For finite or countable $D$ the function $f$ represents the probability distribution directly. For bigger domains $f$ represents the density function. We provide a natural operational semantics for a basic process algebra with this operator and define strong stochastic timed bisimulation and general stochastic bisimulation, which due to the potential uncountable nature of $D$ had to be generalised compared to existing notions. We introduce the notion bisimulation resilience, which restricts the use of the language, such that the bisimulation closure of measurable sets is again measurable, and argue that without such a notion stochastic process expressions make little sense. We prove that the bisimulation equivalences are congruences provided the language is bisimulation resilient.