Completeness of Timed (micron)CRL. Software Engineering (SEN).

摘要

A straightforward extension of the process algebra microCRL was proposed to explicitly deal with time. The process algebra microCRL 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. But contains syntax, operational semantics and axioms characterising timed microCRL. It did not contain an in-depth analysis of timed microCRL. This paper fills this gap by providing soundness and completeness results. The main tool to establish these is a mapping of timed to untimed microCRL and employing the completeness results obtained for untimed microCRL.