Advertisement

Faster Unfolding of General Petri Nets Based on Token Flows

  • Robin Bergenthum
  • Robert Lorenz
  • Sebastian Mauser
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5062)

Abstract

In this paper we propose two new unfolding semantics for general Petri nets combining the concept of prime event structures with the idea of token flows developed in [11]. In contrast to the standard unfolding based on branching processes, one of the presented unfolding models avoids to represent isomorphic processes while the other additionally reduces the number of (possibly non-isomorphic) processes with isomorphic underlying runs. We show that both proposed unfolding models still represent the complete partial order behavior. We develop a construction algorithm for both unfolding models and present experimental results. These results show that the new unfolding models are much smaller and can be constructed significantly faster than the standard unfolding.

Keywords

Partial Order Model Check Event Structure Weak Identical Event Construction Algorithm 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Best, E., Devillers, R.: Sequential and concurrent behaviour in petri net theory. Theoretical Computer Science 55(1), 87–136 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Couvreur, J.-M., Poitrenaud, D., Weil, P.: Unfoldings for general petri nets. University de Bordeaux I (Talence, France), University Pierre et Marie Curie (Paris, France) (2004), http://www.labri.fr/perso/weil/publications/depliage.pdf
  3. 3.
    Desel, J., Neumair, C.: Finite unfoldings of unbounded petri nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 157–176. Springer, Heidelberg (2004)Google Scholar
  4. 4.
    Desel, J., Juhás, G., Lorenz, R.: Viptool-homepage (2003), http://www.informatik.ku-eichstaett.de/projekte/vip/
  5. 5.
    Engelfriet, J.: Branching processes of petri nets. Acta Informatica 28(6), 575–591 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Esparza, J., Heljanko, K.: Implementing ltl model checking with net unfoldings. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 37–56. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  7. 7.
    Esparza, J., Römer, S., Vogler, W.: An improvement of mcmillan’s unfolding algorithm. Formal Methods in System Design 20(3), 285–310 (2002)zbMATHCrossRefGoogle Scholar
  8. 8.
    Goltz, U., Reisig, W.: The non-sequential behaviour of petri nets. Information and Control 57(2/3), 125–147 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Haar, S.: Branching processes of general s/t-systems and their properties. Electr. Notes Theor. Comput. Sci. 18 (1998)Google Scholar
  10. 10.
    Hoogers, P., Kleijn, H., Thiagarajan, P.: An event structure semantics for general petri nets. Theoretical Computer Science 153(1&2), 129–170 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Juhás, G., Lorenz, R., Desel, J.: Can i execute my scenario in your net? In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 289–308. Springer, Heidelberg (2005)Google Scholar
  12. 12.
    Khomenko, V., Kondratyev, A., Koutny, M., Vogler, W.: Merged processes: a new condensed representation of petri net behaviour. Acta Inf. 43(5), 307–330 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Khomenko, V., Koutny, M.: Towards an efficient algorithm for unfolding petri nets. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 366–380. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  14. 14.
    Khomenko, V., Koutny, M.: Branching processes of high-level petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 458–472. Springer, Heidelberg (2003)Google Scholar
  15. 15.
    Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of petri net unfoldings. Acta Inf. 40(2), 95–118 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 164–177. Springer, Heidelberg (1993)Google Scholar
  17. 17.
    Meseguer, J., Montanari, U., Sassone, V.: On the model of computation of place/transition petri nets. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 16–38. Springer, Heidelberg (1994)Google Scholar
  18. 18.
    Meseguer, J., Montanari, U., Sassone, V.: On the semantics of place/transition petri nets. Mathematical Structures in Computer Science 7(4), 359–397 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part i. Theoretical Computer Science 13, 85–108 (1981)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 325–392. Springer, Heidelberg (1987)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Robin Bergenthum
    • 1
  • Robert Lorenz
    • 1
  • Sebastian Mauser
    • 1
  1. 1.Department of Applied Computer ScienceCatholic University of Eichstätt-Ingolstadt 

Personalised recommendations