Title: Concurrency and Probability: Removing Confusion, Compositionally,
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 fully replace nondeterminism with probability distributions and no
stochastic structure is desired/allowed. Here we propose a general solution
based on a recursive, static decomposition of (finite, occurrence) nets in loci
of decision, called structural branching cells (s-cells). Each s-cell exposes a
set of alternatives, called transactions, that can be equipped with a general
probabilistic distribution. The solution is formalised as a transformation from
a given Petri net to another net whose transitions are the transactions of the
s-cells and whose places are the places of the original net, with some
auxiliary structure for bookkeeping. The resulting net is confusion-free,
namely if a transition is enabled, then all its conflicting alternatives are
also enabled. Thus sets of conflicting alternatives can be equipped with
probability distributions, while nonintersecting alternatives are purely
concurrent and do not introduce any nondeterminism: they are Church-Rosser and
their probability distributions are independent. The validity of the
construction is witnessed by a tight correspondence result with the recent
approach by Abbes and Benveniste (AB) based on recursively stopped
configurations in event structures. Some advantages of our approach over AB's
are that: i) s-cells are defined statically and locally in a compositional way,
whereas AB's branching cells are defined dynamically and globally; ii) their
recursively stopped configurations correspond to possible executions, but the
existing concurrency is not made explicit. Instead, our resulting nets are
equipped with an original concurrency structure exhibiting a so-called complete
concurrency property.