Journal of Logic and Computation, Volume 10, Issue 1, pp. 3-42: Abstract.
SPADES - a process algebra for discrete event simulation
PG Harrison1 and B Strulo2
1Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ, UK, E-mail: firstname.lastname@example.org, 2British Telecom Research Laboratory, Martlesham Heath, UK, E-mail: Bstrulo@srd.bt.co.uk
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 specification of a simulation. The algebra is applied to describe quantitatively a range of communicating systems.
Keywords: Simulation, stochastic process algebra, concurrency, transition systems