Concurrency and Probability: Removing Confusion, Compositionally

TL;DR

This paper introduces a static, compositional method to transform Petri nets with confusion into confusion-free nets, enabling probabilistic decision-making while preserving concurrency.

Contribution

It proposes a novel recursive decomposition into structural branching cells, producing confusion-free nets that accurately reflect concurrency and support probabilistic choices.

Findings

Confusion is effectively eliminated in transformed nets.

The approach maintains true concurrency in the resulting nets.

The method is compositional and statically defined.

Abstract

Assigning a satisfactory truly concurrent semantics to Petri nets with confusion and distributed decisions is a long standing problem, especially if one wants to resolve decisions by drawing from some probability distribution. Here we propose a general solution based on a recursive, static decomposition of (occurrence) nets in loci of decision, called structural branching cells (s-cells). Each s-cell exposes a set of alternatives, called transactions. Our solution transforms a given Petri net into another net whose transitions are the transactions of the s-cells and whose places are those of the original net, with some auxiliary structure for bookkeeping. The resulting net is confusion-free, and thus conflicting alternatives can be equipped with probabilistic choices, while nonintersecting alternatives are purely concurrent and their probability distributions are independent. The validity of the construction is witnessed by a tight correspondence with the recursively stopped configurations of Abbes and Benveniste. Some advantages of our approach are that: i) s-cells are defined statically and locally in a compositional way; ii) our resulting nets faithfully account for concurrency.