Free-Choice Nets With Home Clusters Are Lucent

TL;DR

This paper proves that free-choice Petri nets with a home cluster are lucent, meaning each state is uniquely identified by enabled transitions, even if the nets are not live or strongly connected, broadening analysis possibilities.

Contribution

It establishes that free-choice nets with a home cluster are lucent without requiring the nets to be live or strongly connected, offering new analysis perspectives.

Findings

All free-choice nets with a home cluster are lucent.

The approach applies to terminating and initializing systems.

New analysis techniques for non-well-formed nets are enabled.

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 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.