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 |
Email: jfg@cwi.nl |
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
This Page was prepared by Mark Jorgensen.