CCS + time = an interleaving model for real time systems

Abstract

This paper shows how to put time into Milner’s CCS to model real time systems. In particular, we will develop an expansion theorem for real time concurrency, which is an extension of the expansion theorem of CCS. The essential step made in this work is that a more general form of action prefix, μ@t.P is introduced, where t is a time variable. Intuitively, μ@t.P is an agent which may perform μ and become P[d/t] in doing so, where t is replaced by d, the time delay before μ is actually performed. The original form μ.P of action prefix of CCS is just a simple case of μ@t.P when t does not occur free in P — P does not depend on the time at which μ is performed.