Perpetual Free-choice Petri nets are lucent -- proof of a theorem of van der Aalst using CP-exhaustions
arXiv:2109.10002 · doi:10.3233/FI-2021-2078
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.
arXiv commentPublished by Fundamenta Informaticae