a1 Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2AZ, England Email: firstname.lastname@example.org
a2 Department of Computer Science, University of Leicester, University Road, Leicester LE1 7RH, England Email: email@example.com
Van Glabbeek and Goltz (and later Fecher) have investigated the relationships between various equivalences on stable configuration structures, including interleaving bisimulation (IB), step bisimulation (SB), pomset bisimulation and hereditary history-preserving (H-H) bisimulation. Since H-H bisimulation may be characterised by the use of reverse as well as forward transitions, it is of interest to investigate these and other forms of bisimulations where both forward and reverse transitions are allowed. Bednarczyk asked whether SB with reverse steps is as strong as H-H bisimulation. We answer this question negatively. We give various characterisations of SB with reverse steps, showing that forward steps do not add power. We strengthen Bednarczyk's result that, in the absence of auto-concurrency, reverse IB is as strong as H-H bisimulation, by showing that we need only exclude auto-concurrent events at the same depth in the configuration.
We consider several other forms of observations of reversible behaviour and define a wide range of bisimulations by mixing the forward and reverse observations. We investigate the power of these bisimulations and represent the relationships between them as a hierarchy with IB at the bottom and H-H at the top.
(Received April 07 2010)
(Revised January 14 2011)
(Online publication February 28 2012)
§ Irek Ulidowski acknowledges partial support by EPSRC grant EP/G039550/1 and JSPS grants S-09053 and FU-019. He also thanks the University of Leicester for granting study leave.