Structuring acyclic Petri nets for reachability analysis and control (Q5959841)

By structuring the incidence matrices of acyclic Petri nets as a result of a new proof of a well-known reachability condition and of other reachability issues, the authors construct maximally permissive Petri net supervisors guaranteeing that the marking of the original Petri net never leaves a given set. An algorithmic transformation of the original specification into a new one allows taking the presence of uncontrollable transitions into account. The supervisor is obtained by simple matrix multiplication and no linear integer programs need to be solved. In addition, a class of systems is identified for which the maximally permissive supervisor can be realized by extending the standard Petri net enabling condition with OR-logic.