Skip to main content
SpringerLink
Log in

Directed Unfolding of Petri Nets

  • Chapter
Transactions on Petri Nets and Other Models of Concurrency I

Part of the book series: Lecture Notes in Computer Science ((TOPNOC,volume 5100))

Abstract

The key to efficient on-the-fly reachability analysis based on unfolding is to focus the expansion of the finite prefix towards the desired marking. However, current unfolding strategies typically equate to blind (breadth-first) search. They do not exploit the knowledge of the marking that is sought, merely entertaining the hope that the road to it will be short. This paper investigates directed unfolding, which exploits problem-specific information in the form of a heuristic function to guide the unfolding towards the desired marking. In the unfolding context, heuristic values are estimates of the distance between configurations. We show that suitable heuristics can be automatically extracted from the original net. We prove that unfolding can rely on heuristic search strategies while preserving the finiteness and completeness of the generated prefix, and in some cases, the optimality of the firing sequence produced. We also establish that the size of the prefix obtained with a useful class of heuristics is never worse than that obtained by blind unfolding. Experimental results demonstrate that directed unfolding scales up to problems that were previously out of reach of the unfolding technique.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 164–177. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  2. Esparza, J.: Model checking using net unfoldings. Science of Computer Programming 23(2-3), 151–195 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Benveniste, A., Fabre, E., Jard, C., Haar, S.: Diagnosis of asynchronous discrete event systems, a net unfolding approach. IEEE Trans. on Automatic Control 48(5), 714–727 (2003)

    Article  MathSciNet  Google Scholar 

  4. Hickmott, S., Rintanen, J., Thiébaux, S., White, L.: Planning via Petri net unfolding. In: Proc. of 20th Int. Joint Conference on Artificial Intelligence, pp. 1904–1911. AAAI Press, Menlo Park (2007)

    Google Scholar 

  5. Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. Formal Methods in System Design 20(3), 285–310 (2002)

    Article  MATH  Google Scholar 

  6. Esparza, J., Schröter, C.: Unfolding based algorithms for the reachability problem. Fundamentia Informatica 46, 1–17 (2001)

    MathSciNet  MATH  Google Scholar 

  7. Esparza, J., Kanade, P., Schwoon, S.: A negative result on depth first unfolding. Software Tools for Technology Transfer (2007)

    Google Scholar 

  8. Bonet, B., Geffner, H.: Planning as heuristic search. Artificial Intelligence 129(1-2), 5–33 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  9. Hoffmann, J., Nebel, B.: The FF planning system: fast plan generation through heuristic search. Journal of Artificial Intelligence Research 14, 253–302 (2001)

    MATH  Google Scholar 

  10. McDermott, D.: Using regression-match graphs to control search in planning. Artificial Intelligence 109(1-2), 111–159 (1999)

    Article  MATH  Google Scholar 

  11. Murata, T.: Petri nets: properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989)

    Article  Google Scholar 

  12. Chatain, T., Khomenko, V.: On the well-foundedness of adequate orders used for construction of complete unfolding prefixes. Information Processing Letters 104, 129–136 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  14. Cheng, A., Esparza, J., Palsberg, J.: Complexity results for 1-safe nets. In: Shyamasundar, R.K. (ed.) FSTTCS 1993. LNCS, vol. 761, pp. 326–337. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  15. Melzer, S.: Verifikation Verteilter Systeme Mittels Linearer–und Constraint-Programmierung. PhD thesis, Technische Universität München (1998)

    Google Scholar 

  16. Heljanko, K.: Using Logic Programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 240–254. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  17. Khomenko, V., Koutny, M.: LP deadlock checking using partial order dependencies. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 410–425. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  18. Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  19. Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings. Acta Informatica 40(2), 95–118 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  20. Edelkamp, S.: Planning with pattern databases. In: Proc. 6th European Conf. on Planning. LNCS, pp. 13–24. Springer, Heidelberg (2001)

    Google Scholar 

  21. Haslum, P., Bonet, B., Geffner, H.: New admissible heuristics for domain-independent planning. In: Proc. 20th National Conf. on Artificial Intelligence, pp. 1163–1168. AAAI Press / MIT Press (2005)

    Google Scholar 

  22. Pearl, J.: Heuristics: Intelligent Search Strategies for Computer Problem Solving. Addison-Wesley, Reading (1984)

    Google Scholar 

  23. Bylander, T.: The computational complexity of propositional STRIPS planning. Artificial Intelligence 69(1-2), 165–204 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  24. Haslum, P., Geffner, H.: Admissible heuristic for optimal planning. In: Proc. 6th International Conf. on Artificial Intelligence Planning and Scheduling, Breckenridge, CO, pp. 140–149. AAAI Press, Menlo Park (2000)

    Google Scholar 

  25. Corbett, J.C.: Evaluating deadlock detection methods for concurrent software. IEEE Trans. on Software Engineering 22(3) (1996)

    Google Scholar 

  26. Linhares, A., Yanasse, H.H.: Connection between cutting-pattern sequencing, VLSI design and flexible machines. Computers & Operations Research 29, 1759–1772 (2002)

    Article  MATH  Google Scholar 

  27. Edelkamp, S., Jabbar, S.: Action planning for directed model checking of Petri nets. Electronic Notes Theoretical Computer Science 149(2), 3–18 (2006)

    Article  MATH  Google Scholar 

  28. Vogler, W., Semenov, A., Yakovlev, A.: Unfolding and finite prefix for nets with read arcs. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 501–516. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  29. 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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departamento de Computación, Universidad Simón Bolívar, Caracas, Venezuela

    Blai Bonet

  2. National ICT Australia & The Australian National University, Canberra, Australia

    Patrik Haslum & Sylvie Thiébaux

  3. National ICT Australia & The University of Adelaide, Adelaide, Australia

    Sarah Hickmott

Authors
  1. Blai Bonet
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Patrik Haslum
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sarah Hickmott
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sylvie Thiébaux
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Science, Department of Computer Science, IT-parken, University of Aarhus, Aabogade 34, 8200, Aarhus N, Denmark

    Kurt Jensen

  2. Department of Mathematics and Computer Science, Technical University of Eindhoven, Den Dolech 2, 5612 AZ, Eindhoven, The Netherlands

    Wil M. P. van der Aalst

  3. School of Electrical and Information Engineering, University of South Australia, Mawson Lakes Campus, Mawson Lakes, 5095, South Australia, Australia

    Jonathan Billington

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Bonet, B., Haslum, P., Hickmott, S., Thiébaux, S. (2008). Directed Unfolding of Petri Nets. In: Jensen, K., van der Aalst, W.M.P., Billington, J. (eds) Transactions on Petri Nets and Other Models of Concurrency I. Lecture Notes in Computer Science, vol 5100. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89287-8_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-89287-8_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-89286-1

  • Online ISBN: 978-3-540-89287-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation