Skip to main content
SpringerLink
Log in

Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets

  • Conference paper
  • First Online:
Application and Theory of Petri Nets and Concurrency (PETRI NETS 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9115))

Abstract

Petri nets can express concurrency and nondeterminism but not hierarchy. This article presents an extension of Petri nets, in which places can be grouped into so-called “units” expressing sequential components. Units can be recursively nested to reflect the hierarchical nature of complex systems. This model called NUPN (Nested-Unit Petri nets) was originally developed for translating process calculi to Petri nets, but later found also useful beyond this setting. It allows significant savings in the memory representation of markings for both explicit-state and symbolic verification. Five tools already implement the NUPN model, which is also part of the next edition of the Model Checking Contest.

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. Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. In: Proc. ACM SIGSOFT Int. Symp. on Foundations of Software Engineering, pp. 175–188. ACM (1998)

    Google Scholar 

  2. Arora, N.: Comparison of Encoding Schemes for Symbolic Model Checking of Bounded Petri Nets. Master thesis, paper 11511, Iowa State University, USA (2010)

    Google Scholar 

  3. Bernardinello, L., De Cindio, F.: A survey of basic net models and modular net classes. In: Rozenberg, G. (ed.) APN 1992. LNCS, vol. 609, pp. 304–351. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  4. Best, E., Devillers, R., Hall, J.G.: The box calculus: a new causal algebra with multi-label communication. In: Rozenberg, G. (ed.) APN 1992. LNCS, vol. 609, pp. 21–69. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  5. Best, E., Devillers, R.R., Koutny, M.: The box algebra - a model of nets and process expressions. In: Donatelli, S., Kleijn, H. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 344–363. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  6. Best, E., Devillers, R.R., Koutny, M.: A unified model for nets and process algebras. In: Handbook of Process Algebra, chap. 14. Elsevier (2001)

    Google Scholar 

  7. Best, E., Devillers, R.R., Koutny, M.: Petri Net Algebra. EATCS Monographs in Theoretical Computer Science. Springer (2001)

    Google Scholar 

  8. Best, E., Devillers, R.R., Koutny, M.: The Box Algebra = Petri Nets + Process Expressions. Information and Computation 178(1) (2002)

    Google Scholar 

  9. Boudol, G., Castellani, I.: Three equivalent semantics for CCS. In: Guessarian, I. (ed.) Semantics of Systems of Concurrent Processes. LNCS, vol. 469, pp. 96–141. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  10. Boudol, G., Castellani, I.: Flow Models of Distributed Computations: Three Equivalent Semantics for CCS. Information and Computation 114(2) (1994)

    Google Scholar 

  11. Ciardo, G., Zhao, Y., Jin, X.: Ten years of saturation: a Petri Net perspective. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V. LNCS, vol. 6900, pp. 51–95. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  12. de Cindio, F., de Michelis, G., Pomello, L., Simone, C.: Milner’s communicating systems and Petri Nets. In: APN 1982, Informatik-Fachberichte, vol. 66. Springer (1982)

    Google Scholar 

  13. Degano, P., De Nicola, R., Montanari, U.: A Distributed Operational Semantics for CCS Based on Condition/Event Systems. Acta Inf. 26(1/2) (1988)

    Google Scholar 

  14. Devillers, R.R.: Construction of S-invariants and S-components for refined petri boxes. In: Marsan, M.A. (ed.) APN 1993. LNCS, vol. 691, pp. 242–261. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  15. Devillers, R.R.: S-Invariant Analysis of General Recursive Petri Boxes. Acta Informatica 32(4) (1995)

    Google Scholar 

  16. Devillers, R.R., Klaudel, H., Koutny, M., Pommereau, F.: An algebra of non-safe petri boxes. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 192–207. Springer, Heidelberg (2002)

    Google Scholar 

  17. Devillers, R.R., Klaudel, H., Koutny, M., Pommereau, F.: Asynchronous Box Calculus. Fundamenta Informaticae 54(4) (2003)

    Google Scholar 

  18. Dittrich, G.: Specification with nets - report on activities in connection with requirements capture with nets. In: Pichler, F., Moreno-Díaz, R. (eds.) EUROCAST 1989. LNCS, vol. 410, pp. 111–124. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  19. Fehling, R.: A concept of hierarchical Petri Nets with building blocks. In: Rozenberg, G. (ed.) APN 1991. LNCS, vol. 674, pp. 148–168. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  20. Francesco, N.D., Montanari, U., Yankelevich, D.: Axiomatizing CCS, Nets and Processes. Science of Computer Programming 21(3) (1993)

    Google Scholar 

  21. Garavel, H.: Compilation et Vérification de Programmes LOTOS. Doctorate thesis, Université Joseph Fourier (Grenoble), November 1989

    Google Scholar 

  22. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes. Springer International Journal on Software Tools for Technology Transfer (STTT) 15(2), April 2013

    Google Scholar 

  23. Garavel, H., Serwe, W.: State Space Reduction for Process Algebra Specifications. Th. Comp. Sci. 351(2), February 2006

    Google Scholar 

  24. Garavel, H., Sifakis, J.: Compilation and verification of LOTOS specifications. In: Proc. 10th Int. Symp. on Protocol Specification, Testing and Verification (PSTV 1990), North-Holland, June 1990

    Google Scholar 

  25. Garavel, H., Sighireanu, M.: On the introduction of exceptions in LOTOS. In: Proc. Int. Joint Conf. on Formal Description Techniques and Protocol Specification, Testing, and Verification FORTE/PSTV 1996, IFIP. Chapman & Hall (1996)

    Google Scholar 

  26. Goltz, U.: On representing CCS programs by finite Petri Nets. In: Chytil, M., Janiga, L., Koubek, V. (eds.) MFCS 1988. LNCS, vol. 324, pp. 339–350. Springer, Heidelberg (1988)

    Chapter  Google Scholar 

  27. Goltz, U.: CCS and Petri Nets. In: Guessarian, I. (ed.) Semantics of Systems of Concurrent Processes. LNCS, vol. 469, pp. 334–357. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  28. Goltz, U., Mycroft, A.: On the relationship of CCS and Petri Nets. In: Paredaens, J. (ed.) ICALP 1984. LNCS, vol. 172, pp. 196–208. Springer, Heidelberg (1984)

    Chapter  Google Scholar 

  29. Goltz, U., Reisig, W.: CSP-programs with individual tokens. In: Rozenberg, G., Genrich, H.J., Roucairol, G. (eds.) APN 1984. LNCS, vol. 188, pp. 169–196. Springer, Heidelberg (1984)

    Chapter  Google Scholar 

  30. Gorrieri, R., Montanari, U.: Distributed implementation of CCS. In: Rozenberg, G. (ed.) APN 1991. LNCS, vol. 674, pp. 244–266. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  31. Gorrieri, R., Montanari, U.: On the Implementation of Concurrent Calculi in Net Calculi: Two Case Studies. Theoretical Computer Science 141(1&2) (1995)

    Google Scholar 

  32. Hall, J.G., Hopkins, R.P., Botti, O., de Cindio, F.: A Petri Net Semantics of OCCAM2. Tech. report 329, Univ. of Newcastle upon Tyne, Computing Lab. (1991)

    Google Scholar 

  33. Hamez, A., Thierry-Mieg, Y., Kordon, F.: Building Efficient Model Checkers using Hierarchical Set Decision Diagrams and Automatic Saturation. Fundamenta Informaticae 94(3–4) (2009)

    Google Scholar 

  34. Harel, D.: Statecharts: A Visual Formalism for Complex Systems. Sci. Comput. Program. 8(3), 231–274 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  35. He, X.: A formal definition of hierarchical predicate transition nets. In: Billington, J., Reisig, W. (eds.) APN 1996. LNCS, vol. 1091, pp. 212–229. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  36. He, X., Lee, J.: A Methodology for Constructing Predicate Transition Net Specifications. Software, Practice & Experience 21(8) (1991)

    Google Scholar 

  37. He, X., Murata, T.: High-level Petri Nets - extensions, analysis, and applications. In: Electrical Engineering Handbook. Elsevier Academic Press (2005)

    Google Scholar 

  38. Hopkins, R.P., Hall, J.G., Botti, O.: A basic-net algebra for program semantics and its application to OCCAM. In: Rozenberg, G. (ed.) APN 1992. LNCS, vol. 609, pp. 179–214. Springer, Heidelberg (1992)

    Google Scholar 

  39. Huber, P., Jensen, K., Shapiro, R.M.: Hierarchies in coloured Petri Nets. In: Rozenberg, G. (ed.) APN 1991. LNCS, vol. 483, pp. 313–341. Springer, Heidelberg (1989)

    Google Scholar 

  40. ISO/IEC: LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard ISO/IEC 8807 (1989)

    Google Scholar 

  41. ISO/IEC: High-level Petri Nets - Part 2: Transfer Format. International Standard ISO/IEC 15909–2 (2011)

    Google Scholar 

  42. Jensen, K.: Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use. EATCS Monographs on Th. Computer Science, vol. 1. Springer (1992)

    Google Scholar 

  43. Karjoth, G.: Implementing LOTOS specifications by communicating state machines. In: Cleaveland, R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 386–400. Springer, Heidelberg (1992)

    Google Scholar 

  44. Karjoth, G., Binding, C., Gustafsson, J.: LOEWE: A LOTOS Engineering Workbench. Computer Networks and ISDN Systems 25(7) (1993)

    Google Scholar 

  45. Kerbrat, A.: Méthodes Symboliques pour la Vérification de Processus Communicants: Etude et Mise en Œuvre. Doct. thesis, Univ. J. Fourier (Grenoble) (1994)

    Google Scholar 

  46. Kotov, V.E.: An algebra for parallelism based on Petri Nets. In: Winkowski, J. (ed.) MFCS 1978. LNCS, vol. 64, pp. 39–55. Springer, Heidelberg (1978)

    Chapter  Google Scholar 

  47. Kotov, V.E., Cherkasova, L.: On structural properties of generalized processes. In: Rozenberg, G., Genrich, H.J., Roucairol, G. (eds.) APN 1984. LNCS, vol. 188, pp. 288–306. Springer, Heidelberg (1984)

    Chapter  Google Scholar 

  48. Kummer, O., Wienberg, F., Duvigneau, M., Schumacher, J., Köhler, M., Moldt, D., Rölke, H., Valk, R.: An extensible editor and simulation engine for Petri Nets: renew. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 484–493. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  49. Lomazova, I.A.: Nested Petri Nets - a Formalism for Specification and Verification of Multi-Agent Distributed Systems. Fundamenta Informaticae 43(1–4) (2000)

    Google Scholar 

  50. Lomazova, I.A.: Nested Petri Nets: Multi-level and Recursive Systems. Fundamenta Informaticae 47(3-4) (2001)

    Google Scholar 

  51. Montanari, U., Yankelevich, D.: Combining CCS and Petri Nets Via Structural Axioms. Fundamenta Informaticae 20(1/2/3) (1994)

    Google Scholar 

  52. Murata, T.: Petri Nets: Analysis and Applications. Proc. of the IEEE 77(4) (1989)

    Google Scholar 

  53. Nielsen, M.: CCS and its relationship to net theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986 (Part I). LNCS, vol. 255, pp. 393–415. Springer, Heidelberg (1986)

    Chapter  Google Scholar 

  54. Noe, J.D.: Nets in modeling and simulation. In: Brauer, W. (ed.) Net Theory and Applications. LNCS, vol. 84, pp. 347–368. Springer, Heidelberg (1980)

    Chapter  Google Scholar 

  55. Noe, J.D., Nutt, G.J.: Macro E-Nets for Representation of Parallel Systems. IEEE Transactions on Computers C-22(8), August 1973

    Google Scholar 

  56. Olderog, E.R.: Operational Petri Net semantics for CCSP. In: Rozenberg, G. (ed.) APN 1987. LNCS, vol. 266, pp. 196–223. Springer, Heidelberg (1986)

    Chapter  Google Scholar 

  57. Olderog, E.R.: Nets, Terms, and Formulas: Three Views of Concurrent Processes and Their Relationship. Cambridge University Press (1991)

    Google Scholar 

  58. Peterson, J.L.: Petri Nets. ACM Computing Surveys 9(3) (1977)

    Google Scholar 

  59. Suzuki, I., Murata, T.: Stepwise Refinements of Transitions and Places. In: APN 1981, Informatik-Fachberichte, vol. 52. Springer (1981)

    Google Scholar 

  60. Suzuki, I., Murata, T.: A Method for Stepwise Refinement and Abstraction of Petri Nets. Journal of Computer and System Sciences 27(1) (1983)

    Google Scholar 

  61. Taubner, D.: Finite Representations of CCS and TCSP Programs by Automata and Petri Nets. LNCS, vol. 369. Springer, Heidelberg (1989)

    Google Scholar 

  62. Taubner, D.: Representing CCS Programs by Finite Predicate/Transition Nets. Acta Informatica 27(6) (1989)

    Google Scholar 

  63. Valette, R.: Analysis of Petri Nets by Stepwise Refinements. Journal of Computer and System Sciences 18(1) (1979)

    Google Scholar 

  64. Valk, R.: Petri Nets as token objects: an introduction to elementary object nets. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol. 1420, pp. 1–25. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  65. Valk, R.: Object Petri Nets: using the nets-within-nets paradigm. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 819–848. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  66. van Glabbeek, R.J., Vaandrager, F.W.: Petri Net models for algebraic theories of concurrency. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.) PARLE 1987. LNCS, vol. 259, pp. 224–242. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Inria, Grenoble, France

    Hubert Garavel

  2. Université Grenoble Alpes, LIG, 38000, Grenoble, France

    Hubert Garavel

  3. CNRS, LIG, 38000, Grenoble, France

    Hubert Garavel

  4. Saarland University, Saarbrücken, Germany

    Hubert Garavel

Authors
  1. Hubert Garavel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hubert Garavel .

Editor information

Editors and Affiliations

  1. Université Libre de Bruxelles, Brussels, Belgium

    Raymond Devillers

  2. Tampere University of Technology, Tampere, Finland

    Antti Valmari

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Garavel, H. (2015). Nested-Unit Petri Nets: A Structural Means to Increase Efficiency and Scalability of Verification on Elementary Nets. In: Devillers, R., Valmari, A. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2015. Lecture Notes in Computer Science(), vol 9115. Springer, Cham. https://doi.org/10.1007/978-3-319-19488-2_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-19488-2_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-19487-5

  • Online ISBN: 978-3-319-19488-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation