2018/01/12 by Wil M. P. van der Aalst, van der Aalst, Wil M. P. · 1 citation
Business, Management and Accounting · Computer Science · #Business Process Modeling and Analysis #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling #Service-Oriented Architecture and Web Services
paper · pdf · doi:10.48550/arxiv.1801.04315
openalex publication_date 2018/01/12 · openalex created_date 2022/10/04 · openalex updated_date 2026/07/28
A marked Petri net is lucent if there are no two different reachable markings\nenabling the same set of transitions, i.e., states are fully characterized by\nthe transitions they enable. This paper explores the class of marked Petri nets\nthat are lucent and proves that perpetual marked free-choice nets are lucent.\nPerpetual free-choice nets are free-choice Petri nets that are live and bounded\nand have a home cluster, i.e., there is a cluster such that from any reachable\nstate there is a reachable state marking the places of this cluster. A home\ncluster in a perpetual net serves as a "regeneration point" of the process,≠.g., to start a new process instance (case, job, cycle, etc.). Many\n"well-behaved" process models fall into this class. For example, the class of\nshort-circuited sound workflow nets is perpetual. Also, the class of processes\nsatisfying the conditions of the \α algorithm for process discovery falls\ninto this category. This paper shows that the states in a perpetual marked\nfree-choice net are fully characterized by the transitions they enable, i.e.,\nthese process models are lucent. Having a one-to-one correspondence between the\nactions that can happen and the state of the process, is valuable in a variety\nof application domains. The full characterization of markings in terms of\nenabled transitions makes perpetual free-choice nets interesting for workflow\nanalysis and process mining. In fact, we anticipate new verification, process\ndiscovery, and conformance checking techniques for the subclasses identified.\n