6. Analysis

Three different ways of proceeding with the analysis of a net can be distinguished: Reachability analysis, invariant analysis, and structural analysis.

Under reachability analysis, we understand every procedure which relies on a (at least partial) construction of the state or reachability graph of the net. The computation of paths belongs to this category, as well as the computation and analysis of the state graph, where the latter may be computed using symmetric or stubborn set reductions. For unbounded nets, the coverability graph can be computed.

The invariant analysis comprises all processes which aim at the solution of systems of linear equations derived from the incidence matrix of the net. In addition to the classical invariant computation, the simplex-oriented methods, separately described below, also belong to this category.

Structural analysis attempts to obtain results about dynamic properties of the net, such as liveness, based on structural properties, like the deadlock-trap-property.