Bounded Choice-Free Net Synthesis

In the hierarchy of structurally defined Petri net classes, choice-free nets lie above marked graphs, but their reachability graphs are still persistent. Thus, they inherit the properties of Petri nets with persistent reachability graphs. In this chapter, we show that they also enjoy properties that resemble some of the properties of marked graphs. This leads to a rich assortment of necessary synthesisability properties that may be exploited for pre-synthesis and ultimately for synthesis, when a synthesis problem targets a choice-free net.