Abstract:

We explain how we extended mCRL with time in such a way that 'classic' mCRL specifications are valid timed mCRL specifications that only do not make an explicit reference to time. In essence the extension consists of a single at operator, denoted by @. For a process expression p and a time t, p@t means that the first action that p executes must be executed at time t. Using the sum operators and the conditionals, complex time constrains can be expressed.

Furthermore, a distinction has been introduced in the datatypes. In 'classic' mCRL it was only possible to specify that datatypes consisted of a set of constructors. In timed mCRL it is also possible to state that there are ordinary functions which cannot create new elements in the datatype.