REMCONF: A TOOL FOR CONFUSION REMOVAL IN PROBABILISTIC CONCURRENT MODELS

Concurrency and probability are two important features of modern ICT systems, models and languages.

The study of concurrent models where decisions are driven by probabilistic distributions is complicated by the so-called confusion problem. It arises when an event increases or decreases the set of alternatives for another concurrent event that is already enabled.

The confusion problem interferes with concurrency, in the sense that, equivalent computations from point of view of concurrency, can be assigned different probabilities.

In a recent paper it has been shown that confusion can be removed by identifying the loci of decisions and introducing additional dependencies between events.

REMCONF is a tool for the automatic and compositional synthesis of confusion free models, exploiting the theory developed there.

The tool, developed in Java language, receives in input a Petri net (in a suitable class), removes automatically confusion, and produces in output the corresponding transformed Petri net.

The format file for exchanging Petri nets that tool uses is a standard XML dialect called PNML. Therefore, the tool reads a PNML representing the Petri net to transform and outputs another PNML file describing the corresponding Petri net without confusion.

The output Petri net will be described also in DOT format, mainly for a better rendering of its graphical layout.

Petri net with confusion

The occurrence of an event changes the alternatives to a concurrent event

Confusion removal

Confusion can be removed by adding (disjunctive) causal dependencies between events. They are realized by persistent places

REMCONF

  • takes a net in input (PNML format)
  • checks that it is a nondeterministic occurrence net
  • identifies loci of decisions
  • transforms each s-cell in a persistent net fragment
  • assembles all fragments together
  • returns a confusion free persistent net (PNML format/ DOT format)

Steps of the tool

First Step

Take a Petri Net with confusion in PNML format

Second Step

Identify loci of decisions

Third Step

Return a confusion-free Petri Net in DOT format. The figure above is an interpretation in Graphviz.

Fourth step

Return a confusion-free Petri Net in PNML format. The figure above is a runnable net in Woped