Abstract
Concurrency theory and practice provide a useful abstraction for the design and use of a variety of systems. Concurrent computations, as defined in many models, are equivalence classes of execution sequences, where pairs of concurrent events can be executed in any order. Sequences in the same class should be indistinguishable for the current purpose of interest.
Unfortunately, sequences in the same class can behave remarkably differently when choice points are considered: for instance, certain nondeterministic decision points can appear only in some sequences, while in other sequences decision points can be indistinguishable from inessential choices between concurrent events. This problem, called confusion, is a main disadvantage of concurrent models, since it gives evidence that their abstraction level is inadequate for a number of important domains of interpretation, typically probabilistic models.
As for many other issues concerning concurrency, Petri nets provide a simple, well studied, essential touchstone for evidencing the confusion problem, and possibly for solving it.
In particular, a number of probabilistic versions of Petri nets have been proposed in the past years. Most of them replace nondeterminism with probability only in part, and furthermore introduce time dependent stochastic distributions, thus giving up the time and speed independence feature typical of proper concurrent models.
Abbes and Benveniste have recently suggested a convenient solution based on recursively stopped configurations in event structures. However, the concurrent behavior of their model is not fully defined, e.g. in terms of some concurrent transition system.
Here we propose a solution that translates a generic (occurrence) Petri net into a net without confusion, where controversial sequences are not enabled. The mapping is compositional and purely structural/static. We claim that our construction identifies the loci of decision where nondeterminism can be entirely replaced by probabilistic distributions. The construction yields nets with persistent places, as needed by OR-causal dependencies. A simple kind of Asperti-Busi’s dynamic nets is used as an intermediate model to structure the transformation.
This is joint work with Roberto Bruni and Hernán Melgratti. Full paper available at http://arxiv.org/abs/1710.04570.