Embedding untimed into timed process algebra : the case for explicit termination

In ACP-style process algebra, the interpretation of a constant atomic action combines action execution with termination. In a setting with timing, different forms of termination can be distinguished: some time termination, termination before the next clock tick, urgent termination, being terminated. In a setting with the silent action tau , we also have silent termination. This leads to problems with the interpretation of atomic actions in timed theories that involve some form of the empty process or some form of the silent action. Reflection on these problems lead to a re-design of basic process algebra, where action execution and termination are separated. Instead of actions as constants, we have action prefix operators. Sequential composition remains a basic operator, and thus we have two basic constants for termination, delta for unsuccessful termination (deadlock) and epsilon for successful termination (skip). We can recover standard process algebras as subtheories of the new theory. The new approach has definite advantages over the standard approac