Free-Choice Nets With Home Clusters Are Lucent
This provides a foundational result for modeling and analyzing systems in applications requiring lucency, such as process models, though it is incremental as it builds on existing free-choice net theory.
The paper tackles the problem of characterizing lucent Petri nets, where states are uniquely identified by enabled transitions, and proves that all free-choice nets with a home cluster are lucent, enabling new analysis techniques for non-well-formed systems.
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 strongly connected. 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.