CCS + TIME = AN INTERLEAVING MODEL FOR REAL-TIME SYSTEMS

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, mu-@t.P is introduced, where t is a time variable. Intuitively, mu-@t.P is an agent which may perform mu and become P[d/t] in doing so, where t is replaced by d, the time delay before mu is actually performed. The original form mu.P of action prefix of CCS is just a simple case of mu-@t.P when t does not occur free in P - P does not depend on the time at which mu is performed.