Modeling admissible behavior using event signals

We describe here how to obtain a model for the admissible behavior of a discrete event system that is represented by a safe Petri net (PN) model. The transitions of this PN model may be controllable or uncontrollable. Also given is a sequential specification which is modeled with a special state machine. Then, using the condition and event arcs of net condition/event systems, a combined model of plant and specification is obtained. We use only the structure of this combined model to develop a method which gives the admissible behavior of the system. Thus, we avoid the complexity of a complete state enumeration.