English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

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. This paper explores the class of marked Petri nets that are lucent and proves that perpetual marked free-choice nets are lucent. Perpetual free-choice nets are free-choice Petri nets that are live and bounded and have a home cluster, i.e., there is a cluster such that from any reachable state there is a reachable state marking the places of this cluster. A home cluster in a perpetual net serves as a “regeneration point” of the process, e.g., to start a new process instance (case, job, cycle, etc.). Many “well-behaved” process models fall into this class. For example, the class of short-circuited sound workflow nets is perpetual. Also, the class of processes satisfying the conditions of the (alpha ) algorithm for process discovery falls into this category. This paper shows that the states in a perpetual marked free-choice net are fully characterized by the transitions they enable, i.e., these process models are lucent. Having a one-to-one correspondence between the actions that can happen and the state of the process, is valuable in a variety of application domains. The full characterization of markings in terms of enabled transitions makes perpetual free-choice nets interesting for workflow analysis and process mining. In fact, we anticipate new verification, process discovery, and conformance checking techniques for the subclasses identified.

Markings in Perpetual Free-Choice Nets Are Fully Characterized by Their Enabled Transitions