Elimination of duplicate labels in Petri-net-based system specification

Labelled Petri nets are commonly used for system specification where the locations of conditions are denoted as places with condition labels and the locations of events as transitions with event labels. It is often in a Petri-net-based specification that the same condition label or event label appears in multiple locations. As every condition is finally implemented as a unique state and every event as a unique operation, in order for the system specification to become useful for implementation, all duplicate condition labels and event labels must be eliminated. In this paper, we propose a method for eliminating the duplicate labels. Firing sequences are preserved so that the intended system behaviours will not be altered.