Refining and verifying regular Petri nets
Li Jiao · International Journal of Systems Science · 2007
This paper considers two kinds of refinement transformations in terms of places and transitions, and proves that regularity can be preserved automatically for pure and ordinary connected nets under the two refinement transformations. By discussing the relationship between siphons of the original net and the refined net, this paper proves that liveness and boundedness can also be preserved automatically for these refined regular Petri nets. The two property-preserved refinement transformations can be used to construct large and complex net models in Petri-net-based system design and verification. An example coming from the manufacturing system is used to illustrate main results of this paper.