SPADES|a process algebra for discrete event simulation

We present a process algebra, SPADES, based on Milner's CCS, which may be used to describe discrete event simulations with parallelism. It is able to describe the passing of time and probabilistic choice, either discrete, between a countable number of processes, or continuous, to choose a random amount of time to wait. Its operational semantics is presented as a labelled transition system and we discuss equivalences over this operational semantics that imply axioms that can be used to compare and transform processes formally. We discuss notions of equivalence over simulations and the meaning of non-determinism in the context of the specication of a simulation. The algebra is applied to describe quantitatively a range of communicating systems.