Traps characterize home states in free choice systems

Free choice nets are a subclass of Petri nets allowing to model concurrency and nondeterministic choice, but with the restriction that choices cannot be influenced externally. Home states are ground markings which can be reached from any other reachable marking of a system. A trap is a structurally defined part of a net with the property that once it is marked (that is, carries at least one token), it will remain remarked in any successor marking. The main result of this paper characterizes the home states of a live and bounded free choice system by the property that all traps are marked. This characterization leads to a polynomial-time algorithm for deciding the home state property. Other consequences include the proof that executing all parts of a net at least once necessarily leads to a home state; this has been a long standing conjecture.