Abstract
Solving states separation problems is an important technique to obtain liveness-enforcing and optimal or near-optimal supervisors for flexible manufacturing systems based on Petri nets. It first generates the model's reachability graph and partitions it into a live zone (LZ) and a deadlock zone (DZ). Then, first-met bad markings (FBMs), which exist in DZ and are the very first entries from LZ to DZ, are forbidden by some designed place invariants (PIs) to prevent the system from entering DZ. This paper studies the reduction of the number of places to be considered in such PI designs. First, the concepts of critical transitions and critical activity places are defined, and a fast algorithm is provided to compute them. Then, the proofs of that only critical activity places need to be considered in such PI designs to forbid all FBMs and/or permit all legal markings in LZ are established.