LAUSR

This paper focuses on establishing a Petri net (PN)-based deadlock prevention policy for large-scale systems whose state spaces are prone to the explosion problem phenomenon. When using the reachability analysis technique, the main burden is that the number of states grows exponentially with respect to the PN structure and, thereby, synthesizing a lively controlled Petri net model (PNM) becomes an extremely complex procedure. The proposed method reduces the initial marking of the PNM to reduce the size of the reachability graph. Such a reachability graph is reduced exponentially and the activity places are derived iteratively using a well-established invariant-based control method. When the PNM becomes live, the control places are integrated to the original PNM and, therefore, the advantage of this method lies in that the control of the original PN model starts at an earlier stage, i.e., before enumerating the full reachability graph and which we call it one-step control-ahead of a PNM. Compared with the existing methods, the new method requires the control of a very small-sized reachability graph and, therefore, it is convenient for large-scale and bounded PNs. Two examples are used to illustrate the proposed approach. Experimental results show that we can obtain optimal supervisors for the net models.