6.5.1 Reductions of the state graph

In addition to an efficient use of memory, INA optionally offers possibilities to reduce the state graph already during the computation. The aim of the reduction is to find appropriate sub-graphs which represent certain properties of the reachability graph. It is thereby possible, that nodes in these reduced graphs are representatives for whole classes of nodes of the reachability graph, or that only one part of the possible state transitions is considered, so that some arcs and nodes of the reachability graph will not be computed. Furthermore, representations exist for the infinite state graphs of unbounded nets.

The net 2.2 of the dining philosophers will serve as an example for state graph reductions. Its state graph has 393 nodes.

Symmetrical reduction

Many net models have symmetries, which can be exploited for the analysis.

When computing a state (or coverability) graph, all states which are mapped to each other by a symmetry can be identified. In some circumstances, the number of states to be computed is thereby considerably reduced, so that the overall computation (including the determination of the symmetries) can be faster than the one of the complete state graph. The disadvantage of the symmetrically reduced state graph is that, in general, it only allows to make weaker statements about liveness of transitions.

The symmetries are computed either separately, with the function <Y> , or automatically (in case they had not already been), prior to the construction of a symmetrically reduced graph. Only the generators are computed, from which the symmetries can be combined during the construction. In the worst case, a net has an exponential number of symmetries; the number of generators, however, is polynomial in net size. By generating symmetries from the formerly computed generators, an enormous amount of memory can be saved. The procedure implemented here, generally has a good run-time behaviour.

<Y> Compute the symmetries of the net

When computing the symmetry group of the current net, INA considers possible time allocations.

First, you have to state whether fixed points should be set for places and transitions, or whether the initial state should be considered as symmetric: Do you want to set fixpoints or initial state to be symmetric?

Sometimes, other symmetries or none at all are found in this way, and the computation is cancelled: Trivial transition partition or identity is the only symmetry.

By answering the question Write the symmetries to the session file with <Y> , the generators of the symmetry group are written into the session-report. With <N> , only the decompositions of the place and transition sets into equivalence classes are written.

During the computation, a counter records the generators found; the running computation can be aborted with <Q> .

At the end of the computation, the number of generators and the number of symmetries, which can be obtained by combining them, are displayed.

The function <Y> can also be used to have a (already once computed) symmetry group be re-computed. In order to do this, you only have to answer the question compute the symmetries once again? with <Y> . For example, you can set new fixed points, or consider the initial marking.

For the net 2.1 without multiplicities, the computation looks like the following:

......................Do You want to set fixpoints? Y/N N
.....................Initial state to be symmetric? Y/N Y
..........Write the symmetries to the session file? Y/N Y

Generators:           3

Generating set of the symmetries: 

* Places:      (2 3)(5 6)
  Transitions: (2 3)(5 6)

* Places:      (1 2 3)(4 5 6)
  Transitions: (1 2 3)(4 5 6)

* Places:      (1 3 2)(4 6 5)
  Transitions: (1 3 2)(4 6 5)

3 generators for 6 symmetries found!

Classes of equivalent places:
   1:  4.prog1_on_break,  5.prog2_on_break,  6.prog3_on_break,
   2:  1.prog1_at_term,  2.prog2_at_term,  3.prog3_at_term,
   3:  0.terminal_free,

Classes of equivalent transitions:
   1:  4.logout_prog1,  5.logout_prog2,  6.logout_prog3,
   2:  1.login_prog1,  2.login_prog2,  3.login_prog3,

First, the set of generators is displayed in cyclic notation: the first generator means that place 2 is mapped to place 3 and place 5 to place 6 (and vice versa); similarly for the transitions. The first part of the second generator means that place 1 is mapped to place 2, place 2 to place 3, and place 3 to place 1.

Afterwards, the equivalence classes are outputted: the places 1, 2, and 3 are equivalent, as are the places 4, 5, and 6. Place 0 is a singleton set with respect to the decomposition. As for the transitions, 1, 2, and 3 are eqivalent, and so are 4, 5, and 6.

Figure 6.2: Two traffic lights (ampel.pnt)

The net 6.2 is (in contrast to net 2.1) symmetric only without consideration of the initial marking. It models two traffic lights: the places correspond to the colours of the traffic lights (note that this is, nevertheless, not a coloured net). The transitions provide for the necessary traffic security.

A run of the symmetry computation of this net can look like the following:

Computing the symmetries
Do You want to set fixpoints? N
Initial state to be symmetric? Y
Identity is the only symmetry!

Compute the symmetries once again? Y
Do You want to set fixpoints? N
Initial state to be symmetric? N

Generating set of the symmetries: 

* Places:      (3 4)
  Transitions: 

* Places:      (1 2)(3 4)(5 6)
  Transitions: (1 3)(2 4)

2 generators for 4 symmetries found!

Classes of equivalent places:
   1:  5.red_one,  6.rot_two,
   2:  3.yellow_one,  4.yellow_two,
   3:  1.green_one,  2.green_two,

Classes of equivalent transitions:
   1:  2,  4,
   2:  1,  3,

Since the philosophers of net 2.2 have a symmetric behaviour, the computation of the symmetry group is worthwhile: the symmetrically reduced reachability graph has only 47 nodes.

For details, see [Sta90, Kapitel 7 (62-73)], [Sta91], and [SS91]. An up-to-date description of the implementation can be found in [Sch97].

Stubborn reduction

Stubborn reduction is another possibility to decrease the number of nodes of the reachability graph. It can be combined with symmetric reduction; however, it is not available for all net types.

A freedom in the order of firing the transitions (as implied by concurrency) leads to an increase in the number of reachable states. When investigating two different paths leading to the same state, one may find that these paths differ only with respect to the order in which independent, i.e. concurrent transitions are fired. The state graph contains all intermediate states, although some of them are redundant. The aim of stubborn reduction is to construct a smallest possible excerpt from the state graph. In a given marking, only a subset of transitions is fired. This subset is chosen in such a way, that it is influenced as little as possible from other transitions, or only in a specific way already understood. This procedure makes substantial use of the locality principle as well as of concurrency. In this computation, it is in general not sufficient to consider only the enabled transitions, but also some of the transitons which are not enabled. Because it is hard to influence the resulting set, it received the name stubborn set.

The most important properties which can still be deduced are the existence of dead markings and infinite paths.

In net 2.2, the philosophers can act concurrently. The stubbornly reduced reachability graph has 183 nodes. Taking into consideration the previously mentioned symmetries of the net, a reachability graph results from stubborn and symmetric reduction, which is composed of only 28 nodes. In some sense, symmetric reduction is orthogonal to stubborn reduction. Altogether, a possibly drastic reduction of the state graph results - in the example net 2.2, by a factor of ten.

Coverability graphs

For unbounded nets, coverability graphs provide a complete overview of the boundedness of places and the coverability of markings. Their computation is possible only for nets without time allocation and priorities, using the normal firing rule, and therefore is not offered in any other context. INA computes the graph using the algorithm of KARP and MILLER. In case the net is bounded, the coverability graph corresponds to the usual state graph.

For details, see [Sta90, Kapitel 5 (43-53)].

Finkel's Method of computing the minimal coverability graph

In [Fin89], FINKEL considers reachability graphs and coverability graphs as special cases of a more general structure, so-called $\omega$-state graphs. Among all these state graphs, there exists a unique one which is minimal with respect to the number of nodes. For nets without time allocation and priorities, and under the normal firing rule, INA offers the possibility to compute the coverability graph according to FINKEL's method, and thus reduce the number of nodes and arcs during construction. For unbounded nets, a graph results which has fewer nodes than the classical coverability graph. For bounded nets, the additional time expense lies within acceptable limits, but no essential reduction is achieved. The knowledge of the minimal $\omega$-state graph is sufficient to decide properties such as boundedness of the net, coverability of markings, or the existence of infinite paths in the reachability graph.

Figure 6.3: The alternating bit protocol (altbit.pnt)

The net 6.3 is usually considered using the step firing rule, and is then bounded. If this net is analyzed without the step firing rule, it no longer models the alternating bit protocol correctly. Since it is unbounded in this case, it is nonetheless introduced here as an example for a drastic reduction of the state graph. The computation of the classical coverability graph requires several days; the graph has 435316 nodes. Using FINKEL's method, a graph results with 72 nodes, the computation only lasts a few seconds.

For definitions and details of the implementation, see the diploma thesis [Lü95].