Verification methods based on the state space have a major drawback: the reachability graph must be computed in advance. The construction of this reachability graph is computationally a very hard problem. This is because the size of the state space may grow more than exponentially with respect to the size of the Petri net model (measured, for example, by the number of places). This problem is usually known as the state-space explosion problem. In [Va192] the reader can find a discussion of the size of the reachability graph obtained from a Petri net and the role of the concurrency in the state-space explosion problem.
KeywordsLinear Programming Problem Reduction Rule Reachability Graph Input Place Firing Sequence
Unable to display preview. Download preview PDF.