A method for adding counter-places to the incidence matrix of Petri net

It is shown that there are two problems that must be solved when applying a Petri net to an actual case of a sequential control system. The first one is how to divide a large-sized reachability problem into small-size problems that can be solved in a feasible computation time with a computer having a reasonable memory storage capacity. The second problem is how many counter-places would be added and at what positions they should be added. The authors propose a method to divide a Petri net by using the property of place invariants, and add counter-places based on algebraic techniques. An example is given that shows the effectiveness of the approach presented