Decidable reversible equivalences for finite Petri nets

In the context of Petri nets, we survey some behavioral equivalences in the true concurrency spectrum, in order to check which of them are reversible and decidable. Here reversible means that bisimilar markings are able to match not only each other’s forward transitions, but also back- ward ones, by undoing performed events. Equivalently, a behavioural equivalence is reversible iff its coincides with its hereditary version. It is known that the well-studied history-preserving bisimilarity is not reversible, since hereditary history-preserving (hhp) bisimilarity is strictly finer. Hence, we look for reversible, decidable, finer approximations of hhp bisimilarity. As main con- tributions, we show and prove reversible two such equivalences, namely causal-net bisimilarity [Van Glabbeek, 2015] and place bisimilarity [Autant et al., 1991].