Coordinating concurrency to avoid forbidden states in condition models

This paper presents a new way of avoiding and getting around forbidden states in condition models that are used in automated control synthesis of manufacturing systems. The desired high-level behavior of the system is specified by a condition system Petri net called the "Specnet". The forbidden states are defined by a condition system Petri net called "Forbidden condition net". Our manufacturing system is defined by a set of interacting components, which are specified by component models. The high level Spec net is analyzed by a software tool, which converts it to an executable file, which is input to the controller, to control the manufacturing system. In this paper we introduce a new method to avoid and get around forbidden states, by taking the Specnet and the Forbidden condition net as inputs and analyzing the Specnet for the reachability of Forbidden markings, making necessary changes automatically (if needed) in the Specnet, to avoid reaching Forbidden markings, while maintaining the desired high level behavior of the system as defined by the original Specnet.