All the experiments were conducted on a PC with a Pentium 4/2.66 GHz processor and 512MB main memory.
The experiments represent the performance of CPNunf when unfolding CPNs, and that of CPN Tools’ state space methods [8] used for constructing the state space. We used for our experiments CPN Tools version 1.4.
We present only some of the more representative experiments we conducted dur-ing this work. The CP-nets we have chosen (see Appendix) can be divided in two classes: CP-nets involving a lot of concurrency and those without concurrency at all. In each of these classes we have CP-nets that grow on the number of token colours and those that grow on the size, i.e. the number of places and transitions.
We have to add here, that it is not possible to compare CPNunf’s performance with other unfolding tools, since non of the existing unfolders can unfold n-safe CP-nets allowing infinite (as well as finite) sets of colours. The first known high-level Petri net unfolder, PUNF [10], which is as a result of the work in [11, 12], supports only (strictly) 1-safe M-nets (see [11, 12]) and thus not possible to com-pare its performance with that of CPNunf in all of the conducted experiments.
However, we used PUNF to check the correctness of CPNunf for small 1-safe examples. This was done by the conversion of CP-nets into the from PUNF ac-cepted file format.hl_net, using one of the extra features of CPNunf.
5.1 Concurrent CPNs
For our experiments in this class of CP-nets we use the CPN models presented in figures 8(a) and 8(b) in the Appendix.
In Fig.8(a) (Buff(n)) we present a CP-net modelling a buffer of sizen. In Fig.8(b) (FreeStyle(n)) we present a CP-net modelling thefreestyle Dining Philosophers, where we allow the philosophers to eat and think as they want, i.e., they can eat by only using one of the forks. In this case each fork belongs to a philosopher which can be used only by this philosopher.
p1
The experimental results for the unfolding and the state space of these two CP-nets are represented in Table 1 (see Appendix). Reading from the left to the right, in the first column is the numbernwhich represents, e.g., the number of freestyle philosophers (Fig.8(b)) and the number of buffer cells (Fig.8(a)). The second column represents the number of places |P|, and the third column represents the number of transitions|T| of a CP-net. The size of the state space (graph) generated by CPN Tools is shown in the fourth and fifth column, representing the number of states/nodes |N| and the number of arcs |A|, respectively. The sixth, seventh and eighth column represents the size of the prefix generated by CPNunf: |B| = the number of conditions, |E| = the number of events, and
|Ecut| = the number of cut-off events. We have to add here that E represents all events together with the cut-off events inEcut.Brepresents all conditions as well as all conditions in the postset of each cut-off event in Ecut. The last two columns represent the time (in seconds) that CPN Tools and CPNunf need for the generation of the state space and of the finite complete prefix, respectively.
In both examples, Buff(n) and FreeStyle(n), the size of the state space grows exponentially, i.e., 2n. The time for constructing the state space (graph) increases as well, as can be seen in Table 1. While during the unfolding the number of non-cut-off events grows linear to n, i.e., for Buff(n) we have n
i=1i non cut-off events, and forFreeStyle(n) we have 2·n. For the case n= 20 the test for constructing the state space has been interrupted after 16 hours. The size of the state space |N| and the number of arcs |A|, for n = 20, as shown in Table 1, have been calculated by hand according to the previous results for n <20.
5.2 Non Concurrent CPNs
In this class of experiments we have chosen the CP-nets in Fig.9(a) and Fig.9(b) (see Appendix). In the following we will discuss the results for each of the CP-nets.
Conflict pairs The CP-net Conflict(n) in Fig.9(a) represents a CPN model with places on which transition pairs are in conflict with each other, i.e.,n is the number of such places where transition pairs are in conflict. The results are similar for both approaches, state space and unfolding, see Table 1. We did though not construct any larger CP-net, i.e., for n > 31, because it was challenging enough to keep the overview over the CP-net forn= 31, involving 63 places, 62 transitions and 124 arcs. Especially, when constructing it by hand, as we did. Nonetheless, we think that for such nets, even for greater n, both approaches would perform similarly, since these kind of CP-nets are neither complex nor challenging enough. The sizes of the prefix and the state space grow linear to the size of the CP-net, in fact, the state space and the prefix have exactly the same size as the original CP-net.
Sequential We will discuss here the CP-net in Fig.9(b), which models a Pro-ducer/Consumer withn-items. It is a net where only the number of token colours grows, i.e., the number of items to produce and consume. We can observe from the results in Table 1 that forn= 1..20the times for constructing the state space and the prefix are relatively similar. Beginning withn >20the performance of CPNunf starts to let go, and forn = 130 CPNunf needs 2.65 seconds for the construction of the prefix, whereas CPN Tools needs only 0.54 seconds for the state space construction.
Remark: Every time a placepis unfolded, the transitions in the postset of this place are marked (or promoted) as possible extension candidates, and when such a transition is chosen, then the possible correct co-sets are calculated out ofall the copies ofp, i.e., (p,c) token elements in the occurrence net, and the unfolding is extended accordingly.
In our example, the place NextItem is unfolded sequentially, holding different colours, and each time it gets unfolded it promotes transitionproduce, i.e., each time produce is chosen, we calculate all possible co-sets out of 130 instances (conditions in the unfolding) of the placeItems and n≤130 instances of Nex-tItem, depending on how far we have proceeded with the unfolding. We do this, in order not to forget any possible co-set. The problem here is, that each time produce is chosen only one co-set can be built and thus extend the unfolding.
The calculation of co-sets is time consuming, especially when a large number of conditions in the unfolding has to be considered, and this affects the perfor-mance of CPNunf. Thus, CPNunf has a drawback, when a transition has a large number of promoters out of which only one co-set at a time can be built. Prob-ably by saving the information about the already calculated co-sets, one would get better performance. One may ask though, why the performance of CPNunf is still good in the example in Fig.8(b), even though the transitionStart eating has a large number of promoters? Start eating has indeed a large number of promoters, though it gets promoted only once, namely at the beginning when the initial marking is unfolded.
Unfortunately, it was not possible to compare the CPNunf results with PUNF for the Producer/Consumer example, since, as mentioned, PUNF does not
ac-cept n-safe nets, forn >1. Nonetheless, the number of non-cut-off events does not exceed the number of reachable states, and as in the previous example the state space and the prefix grow linear to each other.
6 Conclusions
We have introduced in this paper the branching processes of Coloured Petri Nets, adopted from the approach presented in [11, 12]. In addition we briefly presented our tool, CPNunf, for unfolding finite and n-safe Coloured Petri Nets allowing finite and infinite sets of colours. The experiments show that CPNunf can successfully be used for the prefix generation of Coloured Petri Nets, and that it performs better than CPN Tools’ state space methods [8], when dealing with CPNs with a lot of concurrency, and thus alleviate the state space explosion problem. Nonetheless, CPNunf has its weak points, as was the case with the Producer/Consumer(n) example. This drawback is caused by transitions which have a large number of promoters, since we calculate the co-sets all over again, each time a transition is promoted. Keeping track of the already built co-sets, i.e., not to calculate them each time from the beginning, would probably solve this problem.
The generated prefixes can be used to investigate the behaviour properties of CPNs by applying prefix-based model checkers. We conducted some experiments, which we did not show here, and the results were promising, e.g., we could check the liveness properties for the CP-net Buff(20), whereas with CPN Tools we could not even generate the state space graph.
We think that by extending CPNunf, i.e., to allow other colour sets than INT, and by developing advanced prefix-based model checkers, one can investigate even more efficiently behaviour properties of CPNs.
Acknowledgments
I would like to thank Bernd Finkbeiner at the University of Saarland and Lars M. Kristensen at the University of Aarhus for their valuable advice and support.
My thanks go to Maciej Koutny and Victor Khomenko at the University of Newcastle upon Tyne for their valuable comments and helpful advice on the unfolding technique.
References
1. J. Esparza, S. Römer and W. Vogler: An Improvement of McMillan’s Unfolding Algorithm.Formal Methods in System Design20(3) (2002) 285-310.
2. J. Esparza and C. Schröter: Unfolding Based Algorithm for the Reachability Prob-lem.Fundamenta Informaticae 46 (2001) 1-17.
3. K. Heljanko: Deadlock and Reachability Checking with Finite Complete Prefixes.
Research Reports 56. Helsinki University of Technology (1999).
4. K. Heljanko: Minimizing finite complete prefixes. In Proceedings of the Workshop Concurrency, Specification and Programming (1999) 83-95.
5. K. Jensen (1992)Coloured Petri Nets. Basic Concepts, Analysis Methods and Prac-tical Use. EATCS Monographs on TheorePrac-tical Computer Science.
6. K. Jensen and L. M. Kristensen:Coloured Petri Nets - Modelling and Verification of distributed systems. Draft Manuscript (January 2005).
7. K. Jensen and L. M. Kristensen:Coloured Petri Nets - Modelling and Validation of Concurrent Systems. Lecture Notes (January 2006).
8. K. Jensen, S. Christensen and L. M. Kristensen: CPN Tools State Space Manual.
Manual (2006).
9. V. Khomenko:CLPDocumentation and User Guide. Version 6.01.Manual (2002).
10. V. Khomenko: PUNF Documentation and User Guide. Version 3.01β. Manual (2002).
11. V. Khomenko:Model Checking Based on Prefixes of Petri Net Unfoldings. PhD thesis. University of Newcastle upon Tyne (2003).
12. V. Khomenko and M. Koutny: Branching Processes of High-Level Petri Nets. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003)(2003).
13. V. Khomenko, M. Koutny and W. Vogler: Canonical Prefixes of Petri Net Unfold-ings. InProceedings of the Conference on Computer-Aided Verification (CAV’02) (2002).
14. V. E. Kozura: Unfoldings of Colored Petri Nets. InPerspectives of System Infor-matics. 4th International Andrei Ershov Memorial Conference (PSI 2001)(2001) 268-278.
15. K. L. McMillan: A Technique of State Space Search Based on Unfolding.Formal Methods in System Design 6(1) (1995) 45-65.
16. S. Melzer and S. Römer: Deadlock checking using net unfoldings. InProceedings of the Conference on Computer-Aided Verification (CAV’97)(1997).
17. http://wiki.daimi.au.dk/cpntools
18. http://java.sun.com/xml/jaxb/about.html
19. http://theoretica.informatik.uni-oldenburg.de/˜pep/
Appendix
Buffer(n)
CP−net StateSpaceGraph U nf olding T ime in seconds
n |P| |T| |N| |A| |B| |E| |Ecut|CP N T ools CP N unf
14 28 15 16384 69632 211 106 1 84.76 0.09 15 30 16 32768 147456 241 121 1 335.60 0.12 16 32 17 65536 311296 273 137 1 1250 0.15 17 34 18 131072 655360 307 154 1 5011 0.20 20 40 21 220 220·5.75 421 211 1 - 0.37
FreeStyle(n)
CP−net StateSpaceGraph U nf olding T ime in seconds
n |P| |T| |N| |A| |B| |E| |Ecut|CP N T ools CP N unf
CP−net StateSpaceGraph U nf olding T ime in seconds
n |P| |T| |N| |A| |B| |E| |Ecut|CP N T ools CP N unf
CP−net StateSpaceGraph U nf olding T ime in seconds
n |P| |T| |N| |A| |B| |E| |Ecut|CP N T ools CP N unf
Table 1.State space graph vs. Unfolding.