Structural Methods

  • J. M. Colom
  • E. Teruel
  • M. Silva
  • S. Haddad
Chapter

Abstract

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.

Keywords

Val92 Dition Prefix Monopoly 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • J. M. Colom
  • E. Teruel
  • M. Silva
  • S. Haddad

There are no affiliations available

Personalised recommendations