Binary Information Press
Petri nets are well known for their graphical and analytical capabilities in specification and verification, especially for concurrent systems. Many properties can be analytically defined and many techniques are available for development and verification. In particular, the approach based on property-preserving transformations will be described in more detail in this paper. In the literature, there exist three popular transformations, namely synthesis, reduction, and refinement. Synthesis is an important transformation among them. Different variations of the synthesis problem have been studied in the past. Most of the efforts have been devoted to the decidability problem, i.e. questioning about of the existence of a Petri net with a specified behavior.