Qualitative analysis

Figure 7 presents the selection of qualitative analysis algorithms implemented in QPN-Tool. Apart from `classical' algorithms like reachability graph analysis and calculation of P- and T-invariants, rather new algorithms for special net classes are offered. Qualitative analysis within QPN-Tool aims at liveness and boundedness. If the QPN does not have these properties, information of the employed algorithm is extracted in order to demonstrate the reason for a QPN being unbounded or not live. All implemented qualitative analysis algorithms are based on Petri net theory and ignore timing aspects as firing delays and frequencies and interpret timed places as ordinary places. Properties of this `untimed' QPN carry over to the timed QPN under certain circumstances, if conditions Equal-conflict and Station are satisfied (cf. [3]). Condition Equal-conflict demands that only transitions of the same kind, either timed or immediate, are in conflict and condition Station states that the scheduling strategy has to be of a type like PS or IS. If the QPN is live, bounded and unveils an extended free choice net-structure these conditions are sufficient for the existence of the steady-state distribution.

The choice of algorithms contain:

reachability graph analysis

The algorithm generates the reachability graph and recognises firing sequences of transitions which lead to unbounded markings. The reachability graph is checked and it is determined whether the net is bounded and live. If this is not the case a firing sequence is presented which demonstrates unboundedness or non-liveness.

computation of P- or T-invariants

A system of 'base vectors' for all positive P- and T-invariants is computed.

cover of P- or T-invariants

The algorithm checks whether the net can be covered by positive P- or T-invariant. If not, the set of uncovered places, resp. transitions is presented.

deadlock/trap condition

For the class of simple nets it is possible to ensure liveness by checking the deadlock/trap condition. The algorithm is taken from [16] and generates the set of minimal deadlocks and checks if any minimal deadlock contains a marked trap.

check state-machine-decomposability

The algorithm is taken from [14][13]. It allows to recognise live and bounded Free-Choice nets by checking the net structure. This is highly efficient compared to other analysis algorithms.