Free-choice Nets with Home Clusters are Lucent

Article type: Research Article

Authors: van der Aalst, Wil M.P.^{; *}

Affiliations: Process and Data Science (PADS), RWTH Aachen University, Germany. [email protected]

Correspondence: [*] Address for correspondence: Process and Data Science (PADS), RWTH Aachen University, Germany.

Abstract: A marked Petri net is lucent if there are no two different reachable markings enabling the same set of transitions, i.e., states are fully characterized by the transitions they enable. Characterizing the class of systems that are lucent is a foundational and also challenging question. However, little research has been done on the topic. In this paper, it is shown that all free-choice nets having a home cluster are lucent. These nets have a so-called home marking such that it is always possible to reach this marking again. Such a home marking can serve as a regeneration point or as an end-point. The result is highly relevant because in many applications, we want the system to be lucent and many “well-behaved” process models fall into the class identified in this paper. Unlike previous work, we do not require the marked Petri net to be live and stronglyconnected. Most of the analysis techniques for free-choice nets are tailored towards well-formed nets. The approach presented in this paper provides a novel perspective enabling new analysis techniques for free-choice nets that do not need to be well-formed. Therefore, we can also model systems and processes that are terminating and/or have an initialization phase.

Keywords: Petri nets, Free-Choice Nets, Lucent Process Models

DOI: 10.3233/FI-2021-2059

Journal: Fundamenta Informaticae, vol. 181, no. 4, pp. 273-302, 2021