Liveness enforcement for production systems modeled by time Petri nets

This research reports a liveness enforcement approach in time Petri nets with the control of time intervals of controllable transitions. According to the T-invariants of the timeless counterpart of a time Petri net, a necessary condition is established for the solvability of the liveness enforcement problem. Then, a critical state class graph is designed with the nodes containing critical constraints of the controllable transitions. The existing parametric models to enforce liveness of a time Petri net with controllable and uncontrollable transitions are in general subject to the state explosion issue. To mitigate this problem, we introduce the concept of the first weakly live nodes and transitional nodes to avoid the enumeration of all constraints on unnecessary weakly live nodes. We develop an algorithm to transform a non-live time Petri net into live by controlling the time intervals of controllable transitions. Two production examples are used to illustrate the approach. This approach is efficient since it avoids the extensive enumeration with regard to the constraints on each node in a critical state class graph.