| Summary: | 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.
|
|---|