State Space Analysis of Hierarchical Coloured Petri Nets
8.4. ALGORITHMS AND DATASTRUCTURES 73
empty pack ("pack1",1)
NetPacket Packet
empty
PacketBuffer
[("pack1,1), ("pack2",1)]
Global level
Module level
Multi-Set level
E
e empty
Network 1
2
Site 2 1
State 1 2
Figure 8.8: Representation of states.
states of the CP-net. Figure 8.8 depicts the storage of two states, corresponding to the initial state of the CP-net (GS 1), and the state (GS 2) resulting from an occurrence in the initial state of the transition SendPacket in the instance of the Site module corresponding toSite1. It can be seen that the two GSs share an MS in the site storage (MS 1). This corresponds to the fact that an occurrence ofSendPacketdoes not affect the instance of theSitemodule corresponding toSite2, as explained above. Because the initial state of both instances of theSitemodule is the same, the two corresponding entries in GS 1 refer to MS 1. In a similar way, it can be seen that multi-sets are shared by the MSs.
The representation above avoids unnecessary duplication of complex values and makes it efficient to determine, during the generation of the state space, whether a state resulting from the occurrence of a binding element is already included in the state space. First, the marking of those places which are changed by the occurrence of the binding element is inserted into the Multi-set level. Using the pointers thus obtained, MSs for those modules, whose state is changed by the occurrence of the binding element are created and inserted into the Module level. In this way, pointers into the Module level are obtained for those modules whose state is changed. Pointers into the Module level for the modules whose marking is unchanged are the same as the ones for the marking in which the binding element occurs. Now, given the pointers into the Module level, the marking is already included in the state space if and only if, a GS exists having the same pointers into the Module level and comparing pointers
is an efficient operation. To make insertion in the storages efficient, all storages are organised as search trees.
We now study the effect of using the above sharing of MSs and multi-sets. First, we consider the sharing on the module level for two different configurations of the packet-switch model: three and six packets. For each of the four modules in the CP-net, we compare the number of MSs which should have been stored if no sharing of MSs was made with the number of MSs actually stored. The figures can be found in Tables 8.2 and 8.3. The column Exp depicts the number of MSs which should have been used if no sharing was made. The column Act depicts the actual number of MSs when sharing is used. The column Ratio depicts the actual number divided by the expected number of MSs.
Module Exp Act Ratio
Network 27,100 5,609 ¼½9¾À¿j¾ÁÂsÃ
Site 54,200 28 Ľ9¼À¿j¾ÁÂYÅ
Node 54,200 3 Ľ9ÄÀ¿j¾Á ÂYÆ
Controller 108,400 17 ¾½9ÇÀ¿j¾Á ÂYÅ Total 243,900 5657 ¼½9ÈÀ¿j¾ÁÂYÉ
Table 8.2: Statistics for the Module level - 3 packets.
Module Exp Act Ratio
Network 162,004 25,682 ¾½9ÇÊ¿j¾Á ÂsÃ
Site 324,008 91 ¼½9ËÊ¿j¾Á ÂYÅ
Node 324,008 3 ̽9ÈÊ¿j¾ÁÂYÍ
Controller 648,016 35 Ľοj¾Á ÂYÆ Total 1,458,036 25,811 ¾½9ËÊ¿j¾Á ÂYÉ Table 8.3: Statistics for the Module level - 6 packets.
The Total row shows that the saving in the number of MSs is significant. For example, from the Total row it can be seen that the number of MSs stored is reduced
to¼½9ÈÏ for three packets and¾½9ËÏ for 6 packets.
Let us now consider the sharing of multi-sets. For each type (colour set) in the CP-net, the number of multi-sets which had to be stored if no sharing was done, is compared to the number of multi-sets which is stored, when sharing is done. The figures are shown in Tables 8.4 and 8.5. Again, significant savings are obtained. For example, for 3 packets the number of multi-sets stored was reduced to Á½9¾Î Ï for 3 packets, andÁ½9ÁÄÇÏ for 6 packets.
For the representation of the arcs/binding elements, a single storage is used. For the same reasons as with states, pointers are also used to avoid the duplication of complex values.
8.5. CONCLUSIONS 75
Type Exp Act Ratio
NetPacket 33,654 27 ˽9Áпj¾ÁÂYÅ
Packet 28 4 ¾½Î¿j¾ÁÂsÃ
PacketBuffer 45 11 ¼½Î¿j¾Á ÂsÃ
E 45 2 Î ½Î¿j¾Á ÂYÉ
Capacity 3 3 1.0
Total 33,775 47 ¾½Î¿j¾ÁÂYÑ Table 8.4: Statistics for the Multi-set level - 3 packets.
Type Exp Act Ratio
NetPacket 154,092 51 Ƚ9ÈÀ¿j¾Á ÂYÅ
Packet 91 7 Ò½9ÒÀ¿j¾Á ÂYÉ
PacketBuffer 126 23 ¾½9ËÀ¿j¾Á ÂsÃ
E 126 2 ¾½9ÇÀ¿j¾ÁÂYÉ
Capacity 3 3 1.0
Total 154,428 86 Ľ9ÇÀ¿j¾Á ÂYÅ Table 8.5: Statistics for the Multi-set level - 6 packets.
8.5 Conclusions
In this paper, we have presented a state space tool supporting formal verification, gen-eration of partial state spaces, and analysis of CP-nets based on the capability of draw-ing selected parts of the state space. We also considered the way in which state space analysis is integrated with simulation. A datastructure for a compact representation of state spaces of hierarchical CP-nets was presented and statistics given, demonstrating the applicability of the datastructure.
The recognition of graphical representations of the state space as a means to anal-yse the behaviour of systems has also been considered in a process algebraic setting in [130]. The approaches presented in this paper and in [130] are, however, different.
In [130], the view on the system is specified at the syntactical level and the state space is generated and reduced according to this view. In contrast, we generate the state space once, and then define different views on the system at the semantic (state space) level. To our knowledge the integration between simulation, graphical representation, and state space analysis has not been considered by others.
To some extent, the idea of avoiding duplication of complex values resembles BDDs as, e.g., used in the SMV system [93]. BDDs have indeed proven to be a very compact way in which to represent state spaces, and significant results have been obtained; in particular when the system under consideration exhibits some form of regularity. The data structure presented in this paper avoids, however, some of the potential drawbacks of BDDs. First of all, it does not assume any regularity in the system and is independent of any kind of variable ordering. Furthermore, the memory requirements are more predictable than with BDDs, for which there is no general
cor-relation between the size of the state space and the size of the BDD. In particular, the size of the intermediate BDDs during generation of the state space is often a problem.
The suggested datastructure does not suffer from such “spurious” behaviour. However, the compression obtained by the suggested datastructure is sensitive to the hierarchical structure of the CP-net.
The use of BDDs in the context of Petri Nets has been considered in [100]. The results from [100], which considers k-bounded Petri Nets are not directly applicable to CP-nets, since they rely on encoding/representing the state of a Petri Net as a vector of bits. Due to the elaborated notion of data types and inscription language provided by CP-nets, this is not a priori possible.
The idea of generating partial state spaces has many similarities with on-the-fly model checking as implemented in the SPIN tool [61] for verification of asynchronous process systems. The datastructure used to represent the state space in the SPIN tool has some similarities with the datastructure presented in this paper.
Even taking the above considerations into account, the size of the state spaces re-mains a problem. Several methods for construction of smaller state spaces, preserving many properties, have been proposed in the literature.
One approach is based on the observation that equivalence and symmetry [26, 34, 65, 67] are present in many distributed systems and can be exploited to obtain a reduced state space. A prototype integrated in Design/CPN supporting this approach now exists [78].
An orthogonal approach is based on the observation that one of the main reasons for state explosion is caused by representing all possible interleavings of independent actions. Partial order reduction techniques [124, 136] attempt to avoid representing unnecessary interleavings. Both of the above techniques could be integrated with the ideas of graphical feedback, and the same representation of the state space and the idea of utilising the simulator in the computation of the state space would still work. It is worth observing that the datastructure for representation of the state space presented in this paper already, to a certain extent, takes partial order reduction into account, since a given state of a module is only stored once. State explosion is rarely caused by the individual modules having many different states, but more commonly caused by the cartesian product of the “small” number of states for the individual modules. Hence, by also applying partial order reduction, the main reduction in memory usage would appear at the Global level and in the memory used to store arcs. For practical use of partial order reduction on CP-nets it is important to avoid relying on unfolding to the underlying Place/Transition net. Some results on the use of stubborn sets for CP-nets can be found in [86, 125].
Another approach to obtain a reduced state space is based on compositionality [128] and modularity [21]. Systems, like for instance the packet-switch model con-sidered in this paper, are often specified in a number of modules. The state space of the individual modules is often of a size which can easily be handled. By introducing suitable parallel composition operators and introducing black-box semantics, compo-sitionality in the model of the system can be exploited with respect to verification.