  We design a reversible version of truly concurrent process algebra CTC which
is called RCTC. It has good properties modulo several kinds of strongly
forward-reverse truly concurrent bisimulations and weakly forward-reverse truly
concurrent bisimulations. These properties include monoid laws, static laws,
new expansion law for strongly forward-reverse truly concurrent bisimulations,
\tau laws for weakly forward-reverse truly concurrent bisimulations, and
congruences for strongly and weakly forward-reverse truly concurrent
bisimulations.
