Petri Net Synthesis with Union/Find

摘要

We propose a new algorithm for the synthesis of a Petri net from a transition system. It is presented for a class of place/transition Petri nets we call Δ1-Petri nets. A Δ1-Petri net has an incidence matrix where entries have values 0, 1, and -1 only. This class includes safe Petri nets as well as ordinary place/transition nets. The proposed algorithm can be adapted to these net classes. The algorithm employs Tarjan's union/find algorithm for managing sets of vertices. It requires just O(|V||T|) space where V is the set of vertices and T is the set of transition labels. Consequently, problem instances even beyond 1,000,000 vertices have a manageable memory footprint. Our results are experimentally validated using a prototype implementation.