A method for stepwise refinement and abstraction of Petri nets

AbstractThis paper is concerned with a method for expanding (or reducing) a Petri net representation to the desired level of detail using step-by-step refinement of transitions and places (or abstraction of subnets to transitions). In particular, we present conditions under which a subnet can be substituted for a single transition while preserving properties such as liveness and boundedness. The present method is general enough to include previously reported methods as special cases. The refinement technique can be used as a top-down approach for synthesizing Petri net models of concurrent systems, while the abstraction technique can be used as a “divide-and-conquer” approach to the analysis of Petri nets