A New Property of Choice-Free Petri Net Systems

When a Petri net system of some class is synthesised from a labelled transition system, it may be interesting to derive structural properties of the corresponding reachability graphs and to use them in a pre-synthesis phase in order to quickly reject inadequate transition systems, and provide fruitful error messages. The same is true for simultaneous syntheses problems. This was exploited for the synthesis of choice-free nets for instance, for which several interesting properties have been derived. We exhibit here a new property for this class, and analyse if this gets us closer to a full characterisation of choice-free synthesizable transition systems.