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

J.F. Groote, J. Lanik

Onderzoeksoutput: Boek/rapportRapportAcademic

41 Downloads (Pure)


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.
Originele taal-2Engels
Plaats van productieEindhoven
UitgeverijTechnische Universiteit Eindhoven
Aantal pagina's29
StatusGepubliceerd - 2011

Publicatie series

NaamComputer science reports
ISSN van geprinte versie0926-4515


Duik in de onderzoeksthema's van 'Semantics, bisimulation and congruence results for a general stochastic process operator'. Samen vormen ze een unieke vingerafdruk.

Citeer dit