The syntax and semantics of timed $ mu $ CRL

We define a specification language called `{it timed $mu CRL$'. This language is designed to describe communicating processes employing data and time. Timed $mCRL$ is the successor of $mCRL$ cite{GroPo94a. It differs in two main aspects. It is possible to make explicit reference to time using a new `{it at' operator; $pat{t$ is the process $p$ where the first action must take place at time $t$. Furthermore, a distinction has been made between constructors and functions in the datatypes. Care has been taken that every $mu$CRL specification is also a correct timed $mu$CRL specification with exactly the same meaning.