Gavin Lowe
1993, 27pp.
In this paper we describe a way of modelling communicating processes that display both nondeterministic and probabilistic behaviour. We represent processes by nondeterministic, probabilistic, action (NPA) graphs with three sorts of nodes: action nodes, from which the process may evolve by performing visible actions; probabilistic nodes, from which the process may evolve probabilistically; and nondeterministic nodes, from which the process may evolve nondeterministically.
We define a number of types of "observation" -- such as traces and refusals -- that can be made of processes. For each type of observation, we describe how to abstract a corresponding denotational semantics from an NPA graph, so as to represent a process by a set of probability functions on observations -- one function for each way of resolving the nondeterministic choices.
We illustrate our approach by using it to give a semantic model to a probabilistic version of CSP: we give an operational semantics for the language in terms of NPA graphs, and thus obtain a number of denotational semantic models, representing a process by a set of probability functions on observations.