Safety Control Synthesis for Time Petri Nets

We study some control synthesis problems on an extension of time Petri nets that model a plant and its environment. The time Petri net control model both represents controllable and uncontrollable events, the problem is then to design a function (controller) such that a given property is fulfilled. We focus our analysis on safety properties expressed on the markings of the net and we propose a symbolic method to decide the existence of a controller that ensures these properties. Unlike existing methods on time Petri nets, that assume the net is bounded, the method is applicable for any time Petri nets. A consequence is that it is possible to decide the existence of a controller that k-bounds the plant. A method is then proposed to build a state-based controller and problems raised by the implementation (Zenoness, sampling) of the control function on the plant are discussed