Skip to main content
SpringerLink
Log in

A Symbolic Model Checker for Petri Nets: pnmc

  • Chapter
  • First Online:
Book cover Transactions on Petri Nets and Other Models of Concurrency XI

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

Abstract

Symbolic model checking with decision diagrams is a very efficient technique for handling large models. However, even when using advanced algorithms, model checking tools still need to be carefully written. Indeed, they are both CPU and memory bounded: in addition to the algorithms complexity, the limiting factors are the available memory and how fast computations are performed. Thus, each saved CPU cycle or byte can make the difference between a successful model checker and a failing one.

We present pnmc, a symbolic model checker for Petri Nets, and libsdd, its associated library which implements Hierarchical Set Decision Diagrams and automatic saturation. Reliability aside, choices were always made to favour performance.

The combination of advanced algorithms for symbolic model checking and advanced coding techniques offer very good results as shown in the Model Checking Contest 2015, which is used as a background to present pnmc and libsdd.

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 EPUB and 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

Notes

  1. 1.

    This extension remains backward compatible with Tina.

  2. 2.

    Due to memory alignment requirements, this trick may not be used on some CPU or platforms. However, it’s not a problem on “standard” configurations like Linux/x86.

  3. 3.

    pnmc also ranked second on its first appearance at the 2014 edition.

  4. 4.

    Which means that more than one tool agreed on the result.

  5. 5.

    MCC organizers fixed this issue by requiring a normalized output and by using more significant digits when comparing results.

References

  1. libDDD web site. http://ddd.lip6.fr

  2. Aloul, F.A., Markov, I.L., Sakallah, K.A.: Force: a fast and easy-to-implement variable-ordering heuristic. In: Proceedings of the 13th ACM Great Lakes Symposium on VLSI, GLSVLSI 2003, pp. 116–119. ACM, New York (2003). http://doi.acm.org/10.1145/764808.764839

  3. Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA - construction of abstract state spaces for petri nets and time petri nets. Int. J. Prod. Res. 42(14), 2741–2756 (2004)

    Article  MATH  Google Scholar 

  4. Bollig, B., Wegener, L.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993–1002 (1996)

    Article  MATH  Google Scholar 

  5. Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  6. Burch, J., Clarke, E., McMillan, K.: Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comput. 98(2), 153–181 (1992). Special issue for best papers from LICS90

    Article  MathSciNet  MATH  Google Scholar 

  7. Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.I.: Logical and stochastic modeling with Smart. In: Kemper, P., Sanders, W.H. (eds.) TOOLS 2003. LNCS, vol. 2794, pp. 78–97. Springer, Heidelberg (2003). http://dx.doi.org/10.1007/978-3-540-45232-4_6

    Chapter  Google Scholar 

  8. Ciardo, G., Lüttgen, G., Siminiceanu, R.I.: Saturation: an efficient iteration strategy for symbolic state-space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001). http://www.springerlink.com/content/mbff40ngvw3m8k2b

    Chapter  Google Scholar 

  9. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  10. Couvreur, J.-M., Encrenaz, E., Paviot-Adet, E., Poitrenaud, D., Wacrenier, P.-A.: Data decision diagrams for petri net analysis. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 101–120. Springer, Heidelberg (2002). http://www.labri.fr/publications/mvtsi/2002/CEPPW02

    Chapter  Google Scholar 

  11. Couvreur, J.-M., Thierry-Mieg, Y.: Hierarchical decision diagrams to exploit model structure. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 443–457. Springer, Heidelberg (2005). http://dx.doi.org/10.1007/11562436_32

    Chapter  Google Scholar 

  12. Garavel, H.: Nested-unit petri nets: a structural means to increase efficiency and scalability of verification on elementary nets. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 179–199. Springer, Heidelberg (2015). http://dx.doi.org/10.1007/978-3-319-19488-2_9

    Chapter  Google Scholar 

  13. Hamez, A., Thierry-Mieg, Y., Kordon, F.: Building efficient model checkers using hierarchical set decision diagrams and automatic saturation. Fundam. Inf. 94(3–4), 413–437 (2009). http://dx.doi.org/10.1007/978-3-319-19488-2_9

    MathSciNet  MATH  Google Scholar 

  14. Hong, S., Kordon, F., Paviot-Adet, E., Evangelista, S.: Computing a hierarchical static order for decision diagram-based representation from P/T nets. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) Transactions on Petri Nets and Other Models of Concurrency V. LNCS, vol. 6900, pp. 121–140. Springer, Heidelberg (2012). http://dx.doi.org/10.1007/978-3-642-29072-5_5

    Chapter  Google Scholar 

  15. Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Linard, A., Beccuti, M., Evangelista, S., Hamez, A., Lohmann, N., Lopez, E., Paviot-Adet, E., Rodriguez, C., Rohr, C., Srba, J.: HTML Results from the Model Checking Contest @ Petri Net, 2014th edn. (2014). http://mcc.lip6.fr/2014

  16. Thierry-Mieg, Y., Bérard, B., Kordon, F., Lime, D., Roux, O.H.: Compositional analysis of discrete time petri nets. In: Proceedings of the 1st Workshop on Petri Nets Compositions (CompoNet 2011), vol. 726, pp. 17–31. CEUR, Newcastle, June 2011

    Google Scholar 

  17. Thierry-Mieg, Y.: Symbolic model-checking using its-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231–237. Springer, Heidelberg (2015). http://dx.doi.org/10.1007/978-3-662-46681-0_20

    Google Scholar 

  18. Thierry-Mieg, Y., Poitrenaud, D., Hamez, A., Kordon, F.: Hierarchical set decision diagrams and regular models. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 1–15. Springer, Heidelberg (2009). http://dx.doi.org/10.1007/978-3-642-00768-2_1

    Chapter  Google Scholar 

Download references

Acknowledgments

Part of this work was done at the ISAE-SUPAERO institute.

We are very grateful to Bernard Berthomieu for his guidance in writing the transition relation for Time Petri Nets with discrete semantics.

Finally, none of this work would have been possible without the help of Alban Linard on the first version of the libsdd library, which laid out all the important concepts of the current version.

Author information

Authors and Affiliations

  1. Steery.io, Donneville, France

    Alexandre Hamez

Authors
  1. Alexandre Hamez
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexandre Hamez .

Editor information

Editors and Affiliations

  1. Newcastle University , Newcastle upon Tyne, United Kingdom

    Maciej Koutny

  2. FernUniversität in Hagen , Hagen, Germany

    Jörg Desel

  3. Leiden University , Leiden, The Netherlands

    Jetty Kleijn

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Hamez, A. (2016). A Symbolic Model Checker for Petri Nets: pnmc . In: Koutny, M., Desel, J., Kleijn, J. (eds) Transactions on Petri Nets and Other Models of Concurrency XI. Lecture Notes in Computer Science(), vol 9930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53401-4_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-53401-4_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-53400-7

  • Online ISBN: 978-3-662-53401-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation