Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Encoding Petri Nets into CCS (Technical Report)

Benjamin Bogø, Andrea Burattin, Alceste Scalas

TL;DR

The paper investigates which classes of Petri nets can be encoded into plain CCS while preserving observable behaviour up to weak bisimulation. It introduces a staged encoding pipeline that starts with encoding CCS nets into CCS processes, then reduces free-choice workflow nets to CCS nets, and finally encodes them as weakly bisimilar CCS processes; to broaden applicability, it defines 2-\tau-synchronisation nets and group-choice nets. The main contributions are novel encodings for free-choice workflow nets, the introduction of 2-\tau-synchronisation and group-choice nets, and a practical tool (pn2ccs) for performing the encodings and visualizing results, with proofs laid out in appendices. This work enables applying process-calculus analysis and verification techniques to process-mining outputs, bridging a gap between process mining and the theory of process calculi for concurrent systems.

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.

Encoding Petri Nets into CCS (Technical Report)

TL;DR

The paper investigates which classes of Petri nets can be encoded into plain CCS while preserving observable behaviour up to weak bisimulation. It introduces a staged encoding pipeline that starts with encoding CCS nets into CCS processes, then reduces free-choice workflow nets to CCS nets, and finally encodes them as weakly bisimilar CCS processes; to broaden applicability, it defines 2-\tau-synchronisation nets and group-choice nets. The main contributions are novel encodings for free-choice workflow nets, the introduction of 2-\tau-synchronisation and group-choice nets, and a practical tool (pn2ccs) for performing the encodings and visualizing results, with proofs laid out in appendices. This work enables applying process-calculus analysis and verification techniques to process-mining outputs, bridging a gap between process mining and the theory of process calculi for concurrent systems.

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.
Paper Structure (10 sections, 2 theorems, 11 equations, 15 figures, 2 algorithms)

This paper contains 10 sections, 2 theorems, 11 equations, 15 figures, 2 algorithms.

Table of Contents

  1. Introduction
  2. Contributions and structure.
  3. Related Work
  4. Preliminaries: LTSs, Bisimulations, CCS, Petri Nets
  5. LTSs and bisimulations.
  6. CCS.
  7. Petri nets.
  8. Encoding Petri Nets into CCS, Step-by-Step
  9. Encoding CCS Nets into CCS Processes
  10. Encoding Free-Choice Workflow Nets into CCS Processes

Key Result

theorem thmcountertheorem

Given a CCS net $N = (P, T, F, A, \sigma)$ and an initial marking $M_0$, let the result of applying alg:ccs-net to $N$ and $M_0$ be the CCS process $Q$ and defining equations $\mathcal{D}$. Then, $LTS(N, M_0) \mathrel{\sim} LTS(Q, \mathcal{D})$. The translation time and the size of $(Q, \mathcal{D})

Figures (15)

  • Figure 1: Overview of the relation between Petri net classes and CCS considered in this paper. The arrows show algorithms for converting one class into another class.
  • Figure 2: Neither free-choice or workflow net.
  • Figure 3: Workflow but not free-choice net.
  • Figure 4: Free-choice but not workflow net.
  • Figure 5: Free-choice net and workflow net.
  • ...and 10 more figures

Theorems & Definitions (16)

  • definition thmcounterdefinition: Labeled transition system
  • definition thmcounterdefinition: Strong bisimulation
  • definition thmcounterdefinition: Weak bisimulation
  • definition thmcounterdefinition: CCS syntax
  • definition thmcounterdefinition: LTS semantics of CCS
  • definition thmcounterdefinition: Labelled Petri net
  • definition thmcounterdefinition: Marking
  • definition thmcounterdefinition: Firing rule
  • definition thmcounterdefinition: Workflow net alpha-miner
  • definition thmcounterdefinition: Free-choice net free-choice-nets
  • ...and 6 more