A Process Calculus for Expressing Finite Place/Transition Petri Nets

TL;DR

This paper introduces Multi-CCS, a process calculus extending CCS with atomic and multiparty synchronization, and shows it can represent all finite reduced Petri nets through a novel semantics.

Contribution

It presents the first process calculus with CCS as a subcalculus that can semantically represent all finite reduced P/T Petri nets.

Findings

Multi-CCS has a labeled transition system semantics.

A novel technique maps Multi-CCS to unsafe P/T Petri nets.

Finite-net processes in Multi-CCS can represent all finite reduced P/T nets.

Abstract

We introduce the process calculus Multi-CCS, which extends conservatively CCS with an operator of strong prefixing able to model atomic sequences of actions as well as multiparty synchronization. Multi-CCS is equipped with a labeled transition system semantics, which makes use of a minimal structural congruence. Multi-CCS is also equipped with an unsafe P/T Petri net semantics by means of a novel technique. This is the first rich process calculus, including CCS as a subcalculus, which receives a semantics in terms of unsafe, labeled P/T nets. The main result of the paper is that a class of Multi-CCS processes, called finite-net processes, is able to represent all finite (reduced) P/T nets.