Completeness of timed \(\mu\)CRL. (English) Zbl 1011.68063

Reniers, M. A.; Groote, J. F.; van der Zwaag, M. B.; van Wamel, J.

Fundam. Inform. 50, No. 3-4, 361-402 (2002).

Summary: In [\((*)\) J. Groote, The syntax and semantics of timed \(\mu\)CRL, Technical Report SEN-R9709, CWI (Amsterdam, 1997)] a straightforward extension of the process algebra \(\mu\)CRL was proposed to explicitly deal with time. The process algebra \(\mu\)CRL has been especially designed 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. But \((*)\) contains syntax, operational semantics and axioms characterising timed \(\mu\)CRL. It did not contain an in depth analysis of theory of timed \(\mu\)CRL. This paper fills this gap, by providing soundness and completeness results. The main tool to establish these is a mapping of timed to untimed \(\mu\)CRL and employing the completeness results obtained for untimed \(\mu\)CRL.

MSC:

68Q85

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Keywords:

process algebra; \(\mu\)CRL