In: Proc. 20th Annual Int. Computer Software and Applications Conf. (COMPSAC-96), pages 28-35. 1996.
Abstract: Several formal methods model reactive systems as discrete-event systems (DES). This makes mathematical reasoning about their properties easier and controller synthesis possible. This paper investigates the forbidden state control problem in which a DES is represented as a colored Petri net with a symmetry specification. More specifically, an efficient formal method for synthesizing a controller is provided 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, the proposed avoids the exhaustive search of the state space by exploiting a symmetry specification. Furthermore, this abstraction technique allows a compact representation for the controller. Therefore it performs particularly well when applied to large but structured processes with similar components.
Keywords: colored Petri nets, control systems, formal methods.