We present a process algebra which includes probabilistic features and an explicit real number time. The language is intended to be suitable for the description and analysis of discrete event simulations which include parallelism. We take the well-known process algebra CCS and extend it with a real number time prefixing operator. We also add random choice operators including the ability to choose a time to delay from a continuous distribution. In a novel approach to probability we see it as independent of non-deterministic behaviour. Thus non-determinism occurs in our systems and is our interpretation of parallelism or under-specification of behaviour.
To define the meaning of the language we give a formal operational semantics emphasising how the standard approach needs to be extended to our new constructs. In the same way we extend Milner's bisimulation to cover evolution in time and random choice. This requires study of the measure-theoretic basis of the probabilistic definitions. We also give an alternative approach to denotational semantics based on de Nicola and Hennessy testing which involves generalizing the usual power-domain approach. These semantics both imply equations, many common to either approach, that can be used formally to transform, simplify and analyse simulations. We present a series of examples that demonstrate that the language is high-level and easy to use and understand.
The language is suitable for the description of complex systems with parallelism, whether a specification, an implementation or a discrete event model. Thus it can be used to inter-relate these systems and analyse and transform them rigorously. In particular the equations can be used to "compile" complex but readable descriptions or specifications into, for example, low-level Generalized Semi-Markov Process (GSMP) style descriptions. We note that the language is certainly expressive enough to encode most simulations and in particular any described as GSMPs (under some restrictions).
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.