Synthesis of Live and Bounded Persistent Systems

This paper presents a dedicated Petri net synthesis algorithm for the case that a transition system is finite, live, and persistent. In particular, the paper delineates exactly when and how a structurally persistent net may be constructed, by crystallising, out of a general region-theoretic approach, a minimised set of simplified systems of linear inequalities. This extends previous results where reversibility, instead of liveness, played an important role.