Symbolic Coloring of Petri Nets
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.
KeywordsPetri net Logic controllers SM coloring Decomposition Formal reasoning
- 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.Adamski, M., Karatkevich, A., & Węgrzyn, M. (eds.) (2005). Design of embeded control systems. New York: Springer Science+Business Media Inc.Google Scholar
- 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
- 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.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.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.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
Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 2.5 International License (http://creativecommons.org/licenses/by-nc/2.5/), 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.