We provide soundness and completeness results for the extension of muCRL with time put forward by Groote. The specification language muCRL has been designed especially to deal with data in a process algebraic context. Using the features for data, only a minor extension of the language was needed to obtain a very expressive variant of time. The main tool to establish the completeness result is a mapping of timed to untimed muCRL and employing the completeness results obtained for untimed muCRL.

, , ,
CWI
Software Engineering [SEN]

Groote, J. F., Reniers, M., van Wamel, J. J., & van der Zwaag, M. B. (2000). Completeness of timed $ mu $ CRL. Software Engineering [SEN]. CWI.