Analysis of Boundedness and Safeness in a Petri Net-Based Specification of Concurrent Control Systems

Control systems surround people everywhere. Recent years have witnessed wide development of such systems. This is due to the growing demand for systems that autonomously control our environment. For example, there are lamps that automatically turn on at dusk, heating systems that turn offwhen we go to work, and similar ideas that make our lives easier, cheaper, and more ecological. These so-called smart solutions can be found in various aspects of human life, such as banking, manufacturing, automotive, transportation, medical care, process mining, and others. 

A Petri net is one of the forms of graphical specification and representation of various concurrent control systems. Wide applications of Petri nets can be found in the field of distributed systems, embedded systems, edge computing, manufacturing systems, and cyber-physical systems. They are a useful modeling approach because they are supported by verification, validation, and analytical methods. This way, system designers are able to verify the robustness and reliability of their projected systems.

This chapter provides an in-depth overview of related work. Boundedness and safeness are at the core of various methodologies using the theory of Petri nets. The problems of analyzing the properties of Petri nets, such as boundedness and safeness, were undertaken more than 30 years ago and are still the subject of research. Boundedness is an important feature of various systems, such as manufacturing systems. A bounded Petri net determines a finite number of reachable states. 

In this chapter, novel ideas for possible improvement of Petri nets analysis methods are presented. The proposed algorithms are not only dedicated to larger Petri nets, where, as expounded in detail in the previous chapters, exact methods cannot compute in the assumed time. For larger Petri nets, that is, nets with several and more places, the described algorithms do not provide a perfect solution for all cases because, as discussed earlier, the problems are of exponential character. However, the recent ideas presented in this chapter will certainly support concurrent control designers in the field of modeling and analyzing Petri nets.

Experimental research is an essential element in developing novel algorithms and testing already available solutions for their optimal application. Each proposed algorithm should be evaluated using reference methods in terms of its accuracy and operating time. The algorithms introduced in Chapter 4 were tested experimentally. The conducted research was meant to compare the presented methods with reference algorithms. Here, we also discuss the best application of the selected algorithms in order to verify boundedness and safeness. The benchmark library used in the experiments, containing 234 Petri nets, is part of a Hippo project developed at the University of Zielona Góra. The set of test modules consists of various classes as well as features various levels of complexity of the Petri nets used for the specification of hypothetical and real-life examples of control systems.

This chapter deals with a case study of a Petri net-based specification of a manufacturing system. The purpose of this chapter is to introduce one of the manufacturing systems and to illustrate the proposed analytical methods on a reallife example. This chapter also provides a synthetic summary of the research with the presentation of key innovative elements of the author’s over seven-year work. The chapter comments on the proposition as well as on the contribution of this book. Moreover, it outlines possible directions for further endeavors.