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 preserved 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.