Property Preservation by Petri-Net-Based Refinements in System Design

We motivate and study the refinements of places and transitions in Petri nets. A refinement of Petri nets is a transformation by replacing a simple entity of a system with its functional and operational details. In general, the refined system may become incorrect even if the original system is correct because some of its original properties may have been lost or some undesired properties may have been created. For systems specified in ordinary Petri nets, this paper proposes the conditions imposed on two types of refinements under which the following properties will be preserved: liveness, boundedness, reversibility, and fairness. Such results release the designer´s burden for having to provide different methods for individual properties.