Analysing Petri Nets in a Calculus of Context-aware Ambients

This paper proposes an approach to analysing and verifying Petri nets using a Calculus of Context-aware Ambients (CCA). We propose an algorithm that transforms a Petri net into a CCA process, which can then be analysed and verified using the CCA verification tools. Besides, this demonstrates that CCA is at least as expressive as Petri nets. We illustrate the practicality of our approach using a case study of the dining cryptographers problem.