Completeness of timed µCRL

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

Research output: Contribution to journalArticleAcademicpeer-review

1 Downloads (Pure)


In [25] a straightforward extension of the process algebra mCRL was proposed to explicitly deal with time. The process algebra mCRL 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 [25] contains syntax, operational semantics and axioms characterising timed mCRL. It did not contain an in depth analysis of theory of timed mCRL. This paper fills this gap, by providing soundness and completeness results. The main tool to establish these is a mapping of timed to untimed mCRL and employing the completeness results obtained for untimed mCRL.
Original languageEnglish
Pages (from-to)361-402
JournalFundamenta Informaticae
Issue number3-4
Publication statusPublished - 2002


Dive into the research topics of 'Completeness of timed µCRL'. Together they form a unique fingerprint.

Cite this