Supervisory control of Petri nets using polyhedral regions

We propose to use polyhedral computations to check the reachability and co-reachability of Petri nets, and design supervisors enforcing polyhedral invariance. To this aim, we first state a semi-algebraic behavioral model for Petri nets, derived from the marking equation. From it, we derive explicit characterizations of the sets of k-reachable marking vectors, in terms of polyhedral regions of a real vector space. This permits to calculate the region of reachable marking vectors, when the considered Petri net is bounded, as the projection of an integral polyhedron. The polyhedron is computed using the Γ-algorithm, in polynomial time. We propose an algorithm to this computation. We adapt the method to further compute the polytope of reachable, co-reachable and safe marking vectors, meeting a given set of polyhedral constraints, and finally apply it to design a supervising controller. We illustrate the method on the supervisor design of a simple AGV system.