A collective interpretation semantics for reversing Petri nets

Reversing Petri nets (RPNs) have recently been proposed as a net-based approach to model causal and out-of-causal order reversibility. They are based on the notion of individual tokens that can be connected together via bonds. In this paper we extend RPNs by allowing multiple tokens of the same type to exist within a net and we implement a notion of local reversibility for the model based on the collective token interpretation of Petri nets. The resulting framework allows us to model a form of out-of-causal-order reversibility, a type of reversibility that arises most notably in biological systems. Furthermore, it is lightweight in the sense that it requires no global control and no history needs to be preserved. Furthermore, we provide a mechanism for controlling reversibility by associating transitions with conditions, which guard their execution. We demonstrate the usefulness of the framework by modelling the functioning of the sodium-potassium pump, a system where transition execution is governed by activation conditions and featuring reversible behaviour.