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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Encoding Reversible Petri Nets into CCSK

  • Hernán C. Melgratti,
  • Claudio Antares Mezzina,
  • G. Michele Pinna

摘要

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.