Introduction

The process theories introduced so far describe the main features of imperative concurrent programming without the explicit mention of time. Implicitly, time is present in the interpretation of many of the operators introduced before. In the process a.x, the action a must be executed before the execution of process x. The process theories introduced so far allow for the description of the ordering of actions relative to each other. This way of describing the execution of actions through time is called qualitative time. Many systems though rely on time in a more quantitative way.

Consider for example the following caller process. A caller takes a phone off the hook. If she hears a certain tone, she dials some number. It does not matter which one. If she does not hear the tone, she puts the phone back on the hook. After dialing the number, the caller waits some time for the other side to pick up the phone. After some conversation, the caller puts the phone back on the hook. In case the call is not answered within some given time, the caller gives up and also puts the phone back on the hook.

To be able to describe such systems in process theory in the same framework as untimed systems, many process theories have been extended with a quantitative notion of timing. In extending the untimed process theories with timing a number of fundamental choices have to be made with respect to the nature of the time domain, the way time appears syntactically in the equational theory, and the way time is incorporated semantically.