REFINEMENT OF PETRI-NET-BASED SYSTEM SPECIFICATION

Abstract

For a discrete-event system specified as a labelled Petri net, locations of conditions are denoted as places with condition labels while locations of events are denoted as transitions with event labels. Very often, the same condition label or event label may appear in multiple locations in the system specification. Since 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 an algorithm for this refinement through the fusion of common subnets. Our algorithm has three distinctive features. First, the units of fusing are subnets instead of individual places and transitions. Second, the groups of common subnets identified for fusing are maximal and disjoint so that the fusion needs to be done once. Third, the fusion preserves firing sequences so that the system behaviours will not be altered.