9 - CCS with time delays

Summary

In this chapter we will have a close look at the elegant timed process algebra TCCS introduced by Yi (1990, 1991a, b). Syntactically, TCCS extends CCS with just a single construct, a new prefix ε(d).P that means ‘delay d units of time and then behave as P’. As is the case for a number of other timed process algebras, TCCS takes the view that a real-time system has a two-phase behaviour, phases when the system idles while time passes and phases when the system performs atomic actions, assumed to be instantaneous in time. As we shall see, this separation of concerns – together with other design decisions (e.g. so-called time determinism and maximal progress) – makes for a very elegant TCCS semantics.

Intuition

All the types of reactive system mentioned in Chapter 8 should give us sufficient motivation to describe and analyze formally real-time reactive computations. In the first part of the book, we introduced a collection of languages and models based on the flexible and intuitive idea of communicating state machines, and we argued, by means of several examples, that the resulting formalisms can be used to describe and analyze non-trivial reactive systems. When real-time constraints become important to the proper functioning of reactive systems, we should like to continue building on the time-honoured formalisms we have introduced previously. But are those formalisms sufficiently powerful to describe timing constraints in computation? Can we use them to specify, for instance, features such as timeouts?