This tool encodes BPMN choreography diagrams into Petri nets. The translation follows the encoding introduced in the paper "A Petri Net Semantics for BPMN Choreographies"[1], which gives a formal, provably correct semantics to BPMN choreographies by mapping them onto standard Petri nets.
Every BPMN element is translated into a small Petri net fragment: a set of places, transitions, and flow arcs. Start and end events, tasks, and AND-gateways are encoded directly, with a one-to-one correspondence between the BPMN element and its Petri net counterpart.
XOR- and OR-gateways are more delicate, since a split gateway can choose not to activate some of its outgoing branches. To handle this, the encoding relies on a technique known as Dead Path Elimination (DPE)[2]: alongside the "live" part of the net, a parallel dead propagation net carries tokens along the branches that were not selected. When a branch is skipped, a token still flows through its dead propagation counterpart, marking that path as resolved even though no live token ever reaches it.
Thanks to this mechanism, an OR-join can determine locally, just by looking at the tokens it receives, whether every incoming branch has been resolved (either as live or as dead). This avoids any need for global knowledge of the process state, which is what makes the OR-join gateway notoriously hard to formalize in the BPMN standard.
For an OR-gateway with n outgoing (or incoming) branches, the encoding introduces one transition for every non-empty subset of branches, one for each possible combination of activated paths. The number of transitions therefore grows exponentially with the number of branches.
The encoding is proven correct and complete, considering the limitation presented later, with respect to a reference operational semantics for BPMN choreographies[3]: every step allowed by the BPMN semantics corresponds to a firing in the encoded Petri net, and every firing in the net corresponds to a valid BPMN step.