Well-Formed Free-Choice Petri Nets Revisited

TL;DR

This paper revisits well-formed free-choice Petri nets, introducing semi-T-components to provide a new characterization and emphasizing the symmetry between dual concepts, leading to classical coverability theorems and a duality theorem.

Contribution

It introduces semi-T-components as a new tool for characterizing well-formed free-choice Petri nets and highlights the symmetry between dual concepts, offering a unified proof approach.

Findings

Classical coverability theorems derived for T- and S-components

Duality theorem established for well-formed free-choice nets

Symmetric arguments used to prove key properties

Abstract

The theory of free-choice Petri nets is an established field, initiated in the 1970s by Commoner and Hack at MIT. We revisit well-formed free-choice nets (those admitting markings that are both live and bounded) and provide a new characterization by introducing semi-T-components. This notion is dual to that of semi-S-components, which in turn correspond to the well-known minimal siphons. By highlighting the symmetry between these dual concepts, we derive the classical coverability theorems for T- and S-components, as well as the duality theorem -- stating that a free-choice net is well-formed if and only if its reverse-dual is also well-formed -- using arguments that are as symmetric as possible.