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

J.F. Groote, J. Lanik

Research output: Book/ReportReportAcademic

41 Downloads (Pure)

Abstract

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.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages29
Publication statusPublished - 2011

Publication series

NameComputer science reports
Volume1105
ISSN (Print)0926-4515

Fingerprint

Dive into the research topics of 'Semantics, bisimulation and congruence results for a general stochastic process operator'. Together they form a unique fingerprint.

Cite this