Computing Publications

Publications Home » Process Algebra for Discrete Even...

Process Algebra for Discrete Event Simulation

Ben Strulo

PhD Thesis
Department of Computing, Imperial College of Science, Technology and Medicine. University of London.
October, 1993

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).

GZipped Postscript of full publication (325 kilobytes)
(need help viewing GZipped Postscript files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.