Reverse Bisimulations on Stable Configuration Structures

TL;DR

This paper explores reverse bisimulation concepts on stable configuration structures, demonstrating that reverse and forward transitions can be combined without increasing expressive power, and clarifies conditions under which reverse IB matches hereditary history-preserving bisimulation.

Contribution

It introduces characterizations of reverse step bisimulation and extends Bednarczyk's result by identifying specific conditions where reverse interleaving bisimulation equals HH bisimulation.

Findings

Reverse step bisimulation is characterized with no additional power from forward steps.

Reverse IB matches HH bisimulation when auto-concurrency is absent or events at the same depth are excluded.

Forward and reverse transitions can be combined without increasing the expressive power of bisimulation.

Abstract

The relationships between various equivalences on configuration structures, including interleaving bisimulation (IB), step bisimulation (SB) and hereditary history-preserving (HH) bisimulation, have been investigated by van Glabbeek and Goltz (and later Fecher). Since HH bisimulation may be characterised by the use of reverse as well as forward transitions, it is of interest to investigate forms of IB and SB where both forward and reverse transitions are allowed. We give various characterisations of reverse SB, showing that forward steps do not add extra power. We strengthen Bednarczyk's result that, in the absence of auto-concurrency, reverse IB is as strong as HH bisimulation, by showing that we need only exclude auto-concurrent events at the same depth in the configuration.