Over-Approximative Petri Net Synthesis for Restricted Subclasses of Nets.

We show that, given a finite Its, there is a minimal bounded Petri net over-approximation according to a structural preorder and present an algorithm to compute this over-approximation. This result is extended to subclasses of nets, namely pure Petri nets, plain Petri nets, T-nets, and marked graphs, plus combinations of these properties.