Modeling admissible behavior with net condition/event systems

We address the problem of obtaining a model for the admissible behavior of a discrete event system in the presence of uncontrollable events. We start with a safe Petri net model of the plant and a sequential specification modeled with a special state machine. Then, a combined model of plant and specification is obtained by using the condition and event arcs of net condition/event systems. Using the structure of this combined model, we are able to develop a method to obtain the admissible behavior which avoids the complexity of a complete state enumeration