A colored Petri net-based formal method for the design of control systems

Several formal methods model reactive systems as discrete-event systems (DES). This makes mathematical reasoning about their properties easier and controller synthesis possible. We investigate the forbidden state control problem in which a DES is represented as a colored Petri net with a symmetry specification. More specifically, we provide an efficient formal method for synthesizing a controller which, when combined with the original system, will avoid reaching forbidden states. This problem is decidable if the colored Petri net has finite color sets and bounded places. Unlike conventional methods that explore the entire reachable set of states, our method avoids an exhaustive search of the state space by exploiting a symmetry specification. Furthermore, this abstraction technique allows a compact representation for the controller. Therefore, our method performs particularly well when applied to large but structured processes with similar components