Encoding Petri Nets into CCS (Technical Report)

TL;DR

This paper develops novel methods to encode free-choice and workflow Petri nets into CCS processes, enabling the application of process calculus analysis techniques to process mining models.

Contribution

It introduces new encodings from Petri nets to CCS and proves their weak bisimilarity, bridging process mining and process calculus analysis.

Findings

Encodings produce CCS processes weakly bisimilar to original nets

Enables applying process calculus analysis to process mining models

Extends understanding of Petri net and CCS expressiveness

Abstract

This paper explores the problem of determining which classes of Petri nets can be encoded into behaviourally-equivalent CCS processes. Most of the existing related literature focuses on the inverse problem (i.e., encoding process calculi belonging to the CCS family into Petri nets), or extends CCS with Petri net-like multi-synchronisation (Multi-CCS). In this work, our main focus are free-choice and workflow nets (which are widely used in process mining to describe system interactions) and our target is plain CCS. We present several novel encodings, including one from free-choice workflow nets (produced by process mining algorithms like the alpha-miner) into CCS processes, and we prove that our encodings produce CCS processes that are weakly bisimilar to the original net. Besides contributing new expressiveness results, our encodings open a door towards bringing analysis and verification techniques from the realm of process calculi into the realm of process mining.