From timed $X_t$ to $mu$CRL: combining performance and functional analysis

In this paper we first give short overviews of the modelling languages timed Chi and mCRL. Then we present a general translation scheme to translate timed Chi specifications to mCRL specifications. As timed Chi targets performance analysis and mCRL targets functional analysis of systems, this translation scheme provides a way to perform both kinds of analysis on a given timed Chi system model. Finally, we give an example of a timed Chi system and show how the translation works on a concrete case study.