Encoding Reversible Petri Nets into CCSK

Reversibility in computational models is a crucial aspect for applications such as fault-tolerant computing, distributed systems, and quantum computing. Petri nets provide a well-established formalism for modelling concurrent systems, while CCS (Calculus of Communicating Systems) and its reversible extension, CCSK, offer a process algebraic approach to system specification. In this work, we define a method to encode reversible Petri nets into CCSK, ensuring that the structural properties and execution semantics of the original Petri nets are pre- served in the translation. We build upon previous research on encoding standard Petri nets into CCS and extend it by incorporating communication keys to track causal dependencies, enabling reversibility.