Complex parallel or distributed systems, including real time ones, can be modeled in a compact way by means of high level Petri nets. Among the most efficient verification techniques for Petri nets are partial order model-checking methods (a la McMillan), based on the concept of branching processes. Up to date, these are only applicable to low level Petri nets. A high level net first has to be unfolded into a low level one. This unfolding process often results in an unnecessary space explosion. The paper aims at proposing a high level version of such branching processes which can be defined directly from the high level net model. These are shown to be equivalent to the low level ones. They will become the basic structures on which new really efficient model-checking algorithms can be defined.
展开▼
