Analysis of petri nets by stepwise refinements

摘要

If the firing of a transition in a Petri net is considered non instantaneous, it becomes possible to replace a transition in a net P by another net P′ This allows to proceed the description and the analysis of a control structure by stepwise refinements. The necessary and sufficient conditions on P and P′ for the resulting net to be bounded and live, are given.