next up previous

Final Report of the COST-247 Action

Timed μCRL

Jan-Friso Groote

Centrum voor Wiskunde en Informatica
Specification and Analysis of Embedded Systems
P.O. Box 94079
1090 GB Amsterdam
The Netherlands
Tel. +31-20-5924232
Fax. +31-20-5924199


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.

This presentation has been given during the COST-247 Project Management Committee Meeting (Stirling, United Kingdom, October 13--14, 1997).

COST-247 Working Group(s): 1

Web Links :

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page