Symbolic Coloring of Petri Nets

  • Jacek TkaczEmail author
Part of the Studies in Systems, Decision and Control book series (SSDC, volume 45)


In this chapter two methods of automatic coloring of the Petri nets supported by formal reasoning using monotone Gentzen calculus are presented. Coloring is used to determine the State Machine subnets. The colors help to validate intuitively and formally consistency of all sequential processes in the considered discrete state model. The first of presented methods is based on determination of exact transversals of the concurrency hypergraph. The second method is based on an examination of the relationship between the sets of minimum siphons and traps. Use of the Gentzen calculus allows to obtain additional information (the proof trees) from the reasoning process. The proof trees represent a formal proof of correctness of the calculation performed during the determination of the State Machine subnets. The methods presented in the chapter can be used in design of the reconfigurable logic controllers.


Petri net Logic controllers SM coloring Decomposition Formal reasoning 


  1. 1.
    Adamski, M., & Tkacz, J. (2012). Formal reasoning in logic design of reconfigurable controllers. In Proceedings of 11th IFAC/IEEE International Conference on Programmable Devices and Embedded Systems PDeS’12 (pp. 1–6). Brno, Czech Republic.Google Scholar
  2. 2.
    Adamski, M., Karatkevich, A., & Węgrzyn, M. (eds.) (2005). Design of embeded control systems. New York: Springer Science+Business Media Inc.Google Scholar
  3. 3.
    Ben-Ari, M. (2012). Mathematical logic for computer science (3rd ed.). London: Springer.CrossRefGoogle Scholar
  4. 4.
    Biliński, K., Adamski, M., Saul, J., & Dagless, E. (1994). Petri-net-based algorithms for parallel-controller synthesis. IEE Proceedings – Computers and Digital Techniques, 141(6), 405–412.CrossRefGoogle Scholar
  5. 5.
    Gallier, J. H. (1985). Logic for computer science: Foundations of automatic theorem proving. New York: Harper & Row Publishers.zbMATHGoogle Scholar
  6. 6.
    Girault, C., & Valk, R. (2003). Petri nets for system engineering: A guide to modeling, verification, and applications. Berlin: Springer.CrossRefGoogle Scholar
  7. 7.
    Jensen, K., Kristensen, K., & Wells, L. (2007). Coloured Petri nets and CPN tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer (STTT), 9(3), 213–254.CrossRefGoogle Scholar
  8. 8.
    Karatkevich, A. (2007). Dynamic analysis of Petri net-based discrete systems (Vol. 356). Lecture notes in control and information sciences. Berlin: Springer.Google Scholar
  9. 9.
    Kozłowski, T., Dagless, E., Saul, J., Adamski, M., & Szajna, J. (1995). Parallel controller synthesis using Petri nets. IEE Proceedings – Computers and Digital Techniques, 142(4), 263–271.CrossRefGoogle Scholar
  10. 10.
    Murata, T. (1989). Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4), 541–580.CrossRefGoogle Scholar
  11. 11.
    Tkacz, J. (2007). State machine type colouring of Petri net by means of using a symbolic deduction method. Measurement Automation and Monitoring, 53(5), 120–122.Google Scholar
  12. 12.
    Tkacz, J., & Adamski, M. (2011). Calculation of state machine cover of safe Petri net by means of computer based reasoning. Measurement Automation and Monitoring, 57(11), 1397–1400.Google Scholar
  13. 13.
    Węgrzyn, M., Wolański, P., Adamski, M., & Monteiro, J. (1997). Coloured Petri net model of application specific logic controller programs. In Proceedings of IEEE International Symposium on Industrial Electronics ISIE’97 (Vol. 1, pp. 158–163). Guimarães, Portugal. Piscataway.Google Scholar
  14. 14.
    Wiśniewska, M., Wiśniewski, R., & Adamski, M. (2007). Usage of hypergraph theory in decomposition of concurrent automata. Measurement Automation and Monitoring, 53(7), 66–68.Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 2.5 International License (, which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Authors and Affiliations

  1. 1.Institute of Computer Engineering and ElectronicsUniversity of Zielona GóraZielona GóraPoland

Personalised recommendations