================================================================================
SPECS   J.A. Bergstra & A. Ponse
        "Translation of a muCRL-fragment to I-CRL"


We isolate a basic fragment of muCRL, called ``sequential effective
muCRL", in which processes can only be specified with the basic
operators for alternative, sequential and conditional composition.
Here we provide for any process specifiable in this fragment a
translation to some Extended Finite State Machine (EFSM).  We argue
that this translation is correct wrt. the intended semantics of muCRL
and I-CRL.

The idea is that in effective muCRL we can specify a process in such a
way that the structure of the originating specification defines a
(single) EFSM with the ``same" behaviour in a canonical way. As the
relevant process-specification is in that case defined by a very strict
syntax, we start from sequential muCRL (smuCRL), which constitutes a
more basic and interesting fragment of muCRL.

We mainly describe techniques for extending a smuCRL specification in
such a way that any process of interest is bisimilar with a process
defined in the extension by a process-specification that is suitable
for canonical translation.  Though the proof theory for (effective)
muCRL is yet available, we only show such bisimilarity by means of
examples and refrain from formal proofs.

Next we describe a (canonical) translation for a process specified in
such a restricted way to an EFSM and we argue that the EFSM obtained
from this translation has the ``same" behaviour.  Typical for this
translation is that the resulting EFSMs always have two (control)
states: one ``busy" state, and one state denoting termination.

We then show two alternative approaches, that may lead to EFSMs with a
larger number of states.

We conclude with some remarks on `many-sorted' actions in I-CRL and on
the two alternative approaches.

Problems left open.
We do not consider the question of the translation of processes that
are defined in (non-sequential) effective muCRL to I-CRL.