Synthesis of controllers using symbolic reachability graphs

This paper deals with the control problem of forbidden states in discrete event systems. The plant model is described by a coloured Petri net and its evolving by an optimized state graph, called symbolic reachability graph. The problem is studied in the general framework of Ramadge and Wonham theory considering uncontrollable transitions and under nonblockingness requirement. The synthesis method computes a maximally permissive coloured Petri net controller. First, the symbolic reachability graph is considered to determine the legal behaviour that the plant model should have. Then, the theory of regions is applied in order to generate a maximally permissive controller. This controller is expressed in coloured Petri net terms and, is connected to the plant model. The proposed approach exploits the benefits of the parameterized modeling power of coloured Petri nets as well as the reduced size of the symbolic reachability graph.