  Process algebra ACP based on the interleaving semantics can not be reversed.
We design a reversible version of APTC called RAPTC. It has algebraic laws of
reversible choice, sequence, parallelism, communication, silent step and
abstraction, and also the soundness and completeness modulo strongly
forward-reverse truly concurrent bisimulations and weakly forward-reverse truly
concurrent bisimulations.
