Perpetual Free-choice Petri nets are lucent -- proof of a theorem of van der Aalst using CP-exhaustions

TL;DR

This paper proves van der Aalst's theorem for perpetual free-choice Petri nets by exhaustively analyzing CP-subnets, providing a new elementary proof approach for process model analysis.

Contribution

It introduces a novel proof of van der Aalst's theorem using CP-exhaustions, enhancing understanding of Petri net properties.

Findings

Perpetual free-choice Petri nets are lucent.

CP-exhaustions effectively analyze Petri nets.

Elementary methods suffice for the proof.

Abstract

Van der Aalst's theorem is an important result for the analysis and synthesis of process models. The paper proves the theorem by exhausting perpetual free-choice Petri nets by CP-subnets. The resulting T-systems are investigated by elementary methods.