Probabilistic GSOS

In this talk we present the content of a forthcoming CWI technical report, which introduces and discusses an operator specification format for labelled probabilistic transition systems. Because of its similarity to the known GSOS rules for nondeterministic systems, the format is called probabilistic GSOS. Early this year, we have already outlined the development at an ACG meeting. Compared to that presentation, the format now includes transition labels and its correspondence with a categorical specification format - from which a number of well-behavedness results can be derived easily - is proved in detail. We will sketch the argument and give example specifications.  

hosted by