| Summary: | Petri nets are a well-known model of concurrency and provide an ideal setting
for the study of fundamental aspects in concurrent systems. Despite their
simplicity, they still lack a satisfactory causally reversible semantics. We
develop such semantics for Place/Transitions Petri nets (P/T nets) based on two
observations. Firstly, a net that explicitly expresses causality and conflict
among events, for example an occurrence net, can be straightforwardly reversed
by adding a reverse transition for each of its forward transitions. Secondly,
given a P/T net the standard unfolding construction associates with it an
occurrence net that preserves all of its computation. Consequently, the
reversible semantics of a P/T net can be obtained as the reversible semantics
of its unfolding. We show that such reversible behaviour can be expressed as a
finite net whose tokens are coloured by causal histories. Colours in our
encoding resemble the causal memories that are typical in reversible process
calculi.
|
|---|