Our aim is to exploit the FDR model checker for descriptions of
concurrent systems written in the RAISE Specification Language (RSL).
To do this we define a translation from RSL to CSPM, show that the
translation is a strong bisimulation, and then that various properties are
preserved by strong bisimulation.  This allows us to infer properties of the
RSL description  from the results of running FDR.