Perpetual Free-choice Petri Nets are Lucent Proof of a Theorem of van der Aalst Using CP-exhaustions

Article type: Research Article

Authors: Wehler, Joachim^{; *}

Affiliations: Department of Mathematics, Ludwig-Maximilians-Universität München (LMU Munich), München, Germany. [email protected]

Correspondence: [*] Address for correspondence: Department of Mathematics, Ludwig-Maximilians-Universität München, Theresienstrasse 39, D-80333 München, Germany.

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.

Keywords: Free-choice system, CP-subnet, perpetuality, lucency

DOI: 10.3233/FI-2021-2078

Journal: Fundamenta Informaticae, vol. 182, no. 4, pp. 363-393, 2021