Abstract: This article deals with supervisory control problem for coloured Petri (CP) nets. Considering a CP-net, we build a condensed version of the ordinary state-space, namely the symbolic reachability graph (SRG). This latter graph allows to cope with state-space explosion problem for symmetric systems. The control specification can be expressed in terms of either forbidden states or forbidden sequences of transitions. According to these specifications, we derive the controller by applying the theory of regions on the basis of the SRG. Thanks to expressiveness power of CP-nets, the obtained controller to be connected to the plant model is reduced to one single place.
Abstract: 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.
Abstract: This paper reviews a proposal for the modular analysis of Petri nets. It improves the modularity of the verification process using modular state spaces. By adding some computations during the construction of the modular state space, one can determine the liveness of a module without exploring other local information. Thereby, it is suitable for the conception of a new distributed verification approach where every site maintains one module. The sites need to cooperate only during the construction of the modular state space.
