Efficient Method for Checking the Existence of a Safety/ Reachability Controller for Time Petri Nets

This paper considers the Time Petri Nets (the TPN model) with controllable and uncontrollable transitions. It proposes a completely forward on-the-fly algorithm for checking the existence of a safety / reachability controller. Given a TPN and a safety / reachability property, the control consists of restricting the firing intervals of controllable transitions so that to satisfy the property of interest. Our approach, based on the TPN state class graph method, computes on-the-fly the reachable state classes of the TPN while collecting progressively subclasses to be avoided so that to satisfy the property. Three levels of control can be carried out: a static control (independent of states and markings), a marking depending control, or a state depending control. Our approach does not need to compute controllable predecessors and then split state classes as it is the case for other approaches based on exploration of state space of the system (backward and forward approaches).