# Verification of the Boundedness Property in a Petri Net-Based Specification of the Control Part of Cyber-Physical Systems

Marcin Wojnakowski, Remigiusz Wiśniewski

► To cite this version:

Marcin Wojnakowski, Remigiusz Wiśniewski. Verification of the Boundedness Property in a Petri Net-Based Specification of the Control Part of Cyber-Physical Systems. 12th Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS), Jul 2021, Costa de Caparica, Portugal. pp.83-91, 10.1007/978-3-030-78288-7_8. http-03685916

HAL Id: hal-03685916

https://inria.hal.science/hal-03685916

Submitted on 2 Jun 2022

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Verification of the Boundedness Property
in a Petri Net-based Specification
of the Control Part of Cyber-Physical Systems

Marcin Wojnakowski, Remigiusz Wiśniewski

Institute of Control and Computation Engineering, University of Zielona Góra,
65-516 Zielona Góra, Poland

{M.Wojnakowski, R.Wisniewski}@issi.uz.zgora.pl

**Abstract.** A method of analysis of a control part of the cyber-physical system described by a Petri net is presented in the paper. In particular, boundedness of the system is examined. Contrary to other well-known techniques, the proposed idea does not require obtaining of all place invariants, nor computation of all reachable states in the net. Therefore, it is possible to check the boundedness of a net in a more effective and efficient way, compared to the traditional, well-known methods. Furthermore, the proposed algorithm has been examined experimentally with a set of 243 benchmarks (Petri nets). The research results show the high efficiency of the proposed method, since a solution was found even for such nets where popular techniques were not able to analyse boundedness of the system. Finally, the presented idea is illustrated by a case-study real-life example.

**Keywords:** boundedness, Petri nets, control part of cyber-physical systems, invariants, linear algebra.

# 1 Introduction and Problem Formulation

Petri nets are popular state-transition systems that allow for comfortable and easy specification of concurrent systems [1]–[4]. They offer the possibility of graphical modelling, as well, as a wide opportunity of analysis techniques [3], [5], [6]. Recently, Petri nets have become particularly popular in the modelling of the control part of the cyber-physical systems [7]–[9]. A cyber-physical system (CPS) [7], [10] combines computation with physical routes. The behaviour of a CPS is defined by two parts: the cyber and the physical parts [11]. Such systems join physical processes, networks and the computational modules of the system. A CPS finds applications in various fields of human life, for instance medical systems [12], vehicular systems [13], power electronic converters [14] and smart homes [15].

This work focuses on the analysis of the control part of the cyber-physical systems, which plays the computational part of the system. A Petri net-based approach benefits the verification of the design even at the specification phase, allowing a reduction in time and costs of the design of CPS [3], [8]. A very important property of a Petri net-
based system is boundedness [1], [2], [5]. Various design methods require this property in their inputs (cf. [6], [8], [9], [16], [17]). Furthermore, boundedness is an essential in case of systems that are oriented on the implementation in the hardware (for example within the field programmable gate arrays, FPGAs).

The two most popular methodologies for boundedness examination of a Petri net are one which applies linear algebra (place invariants computation [5], [18]), and another which involves reachability tree exploration [19]. However, they are seriously limited, since the number of invariants (or reachable states, respectively) can be exponential [2], [4], [5]. So-called *state explosion problem* may be a real challenge to the designer during the analysis of the system. Usually, in such a case the solution is not found within the assumed time due to the exponential computational complexity.

In the paper a technique for the boundedness verification of the Petri net-based CPS is proposed. The method does not involve computation of all invariants in the system, thus it is more efficient and effective compared to the most popular techniques. The idea of the presented solution is based on the computation of the reduced set of the place invariants. The main contributions are as follows:

* A method that allows for the boundedness verification of the control part of a Petri net-based CPS is proposed.

* The presented technique allows for the efficient boundedness verification of the system, which means that the solution is found in the assumed time.

* The idea has been validated and verified experimentally in order to confirm its efficiency and effectiveness.

* The algorithm is explained by a case-study real-life example of a CPS.

## 2 Petri Nets in Applied Artificial Intelligence Systems

Application of various Petri net-based aspects can be found in the artificial intelligence systems. In particular, boundedness property may play important role in analysis and verification of such systems. Let us briefly present the possible applications that show relations between Petri nets and Applied AI.

Analysis and modelling aspects of multi-agent systems are considered in [20]. The paper studies several important properties of Petri net-based systems, including boundedness and liveness. As stated by the Authors, those features are applicable in the modelling of multi-agent systems. In particular, the system is verified against the deadlocks by analysis of boundedness and liveness properties.

Application of Petri nets for intelligent control and supervision is shown in [21]. The Authors propose a modelling tool called Continuous Fuzzy Petri Net (CFPN). Such a net can be used for the improvement of the performance and optimization of the system. Moreover, CFPNs are applicable in fault tolerance and diagnostics (e.g., to help the operator in the controlling and monitoring of thousands of actuators and sensors). The idea is explained by an example of a water treatment plant.

The overview of scheduling, planning and control of manufacturing systems with the application of AI-based search methods and Petri nets is presented in [22]. The paper focuses on the various aspects, starting with Petri nets and their utilization
in the modelling of manufacturing systems. Then, scheduling techniques are presented, including combination of Petri nets and AI-based heuristic search methods.

## 3 Definitions and Notations

The presented definitions correspond to the notations shown in [2], [4], [5], [24], [25].

**Definition 1.** A Petri net $N$ is a 4-tuple: $N = (P, T, F, M_0)$, where $P$ is a set of places, $T$ is a set of transitions, $F \subseteq (P \times T) \cup (T \times P)$ is a set of arcs, $M_0: P \to \mathbb{N}$ is an initial marking.

**Definition 2.** An incidence matrix $A_{|T| \times |P|}$ of a Petri net $N = (P, T, F, M_0)$ is given by:

$$ a_{ij} = \begin{cases} -1, & (p_j, t_i) \in F \\ 1, & (t_i, p_j) \in F, \\ 0, & \text{otherwise} \end{cases} $$

where cell $a_{ij}$ of matrix $A$ refers to transition $t_i$ and place $p_j$.

**Definition 3.** A place invariant (p-invariant) of a Petri net $N = (P, T, F, M_0)$ is an integer vector such that $A\vec{x} = 0$.

**Definition 4.** A Petri net $N = (P, T, F, M_0)$ is covered by place invariants if every place $p \in P$ belongs to at least one p-invariant.

**Definition 5.** A Petri net $N = (P, T, F, M_0)$ is said to be bounded if there is no marking (state) $M_n$ such that any place $p \in P$ contains more than a finite number of tokens. A Petri net $N$ bounded for any finite initial marking $M_0$ is said to be structurally bounded.

**Theorem 1.** A Petri net $N = (P, T, F, M_0)$ is structurally bounded if it is covered by p-invariants [19].

## 4 The Idea of the Proposed Method

This section presents the idea of the proposed technique. Firstly, we will show the main steps of the proposed method, supplemented by an adequate description. Next, the case study example of the boundedness verification of the real-life cyber-physical system is presented.

The proposed method includes the following steps:

1. Initialization:
a) Read incidence matrix $A_{|T|\times|P|}$ of Petri net $N = (P, T, F, M_0)$ that describes the control part of the cyber-physical system.

b) Form the unit matrix $Q = [D_{|P|\times|P|}|A_{|T|\times|P|}^T]$, where $D$ is an identity matrix, and $A_{|T|\times|P|}^T$ is the transposed incidence matrix of $N$.

c) Initialize the place invariants cover: $C = \emptyset$.

2. Searching for the place-invariants cover: for each column $t \in T$ in $A_{|T|\times|P|}^T$:

a) Find all pair of rows that annul the $j$-th transition (column) of $A^T$ and add them to the matrix $Q$.

b) Find all rows which the intersection with the $j$-th transition (column) is not equal to 0 and delete them from $Q$.

c) Find all rows that cover binary the other ones and delete them from $Q$.

d) Boundedness verification: for each row $r$ of $A^T$ such that all entries of $r$ are equal to 0:

* add place invariant $I$ that refer to the row $r$ in $D$ to the set $C: C = C \cup \{I\}$ (i.e., values of $I$ refer directly to the row $r$ in the matrix $D$),

* examine, whether $C$ covers all places in the net:

- break if $C$ covers all places, the system is structurally bounded;

- otherwise, execute the algorithm from step 2(a).

3. Boundedness verification:

* if the net is covered by place invariants, **the system is structurally bounded**,

* otherwise, its **boundedness of the system is not determined**.

The presented method involves linear algebra. It is based on the technique initially proposed in [18], however it does not require computation of all place invariants in the Petri net. The algorithm works as follows. Initially, the unit matrix $Q$ of matrices $D$ and $A^T$ is formed. Matrix $D$ is initially equal to the identity matrix, while $A^T$ denotes the transposed incidence matrix of the Petri net. Next, the method searches for the invariants by transformations of the matrix $Q$. In particular, subsequent transitions are examined in order to zeros matrix $A^T$. Meanwhile, matrix $D$ holds partially obtained invariants. If any row of $A^T$ is completely zeroed (that is, all its entries are equal to 0), the proper invariant can be obtained from matrix $D$. The algorithm verifies existence of new invariants at each stage, add adds them to the set $C$. The method finishes, once the set $C$ covers all the places.

Let us now explain the proposed algorithm with a real-life example. Figure 1 shows a Petri net-based control system responsible for managing a multi-robot, initially presented in [26]. There are nine places and six transitions in the net, denoted by $p_1, \dots, p_9$ and $t_1, \dots, t_6$, respectively. The system involves pick-and-place operations in order to transfer or obtain parts by two robot arms. Places $p_1, \dots, p_3$, and transitions $t_1, \dots, t_3$ refers to the activities of robot first arm. Similarly, places $p_4, \dots, p_6$, and transitions $t_4, \dots, t_6$ are related to the second arm. The presented example focuses on the collision-free movements. Therefore, only one robot arm is able to access the workspace at a time. The activities in common workspace are represented by places $p_3$ and $p_6$. The collision-free movements are secured by the mutual exclusion technique, and involvement of place $p_7$ (places $p_8$ and $p_9$ are used as additional buffers).
<figure><img src="image_2.png" /><figcaption>Fig. 1. A multi-robot controller specified by a Petri net.</figcaption></figure>

Let us now examine the boundedness of the system with the proposed method. According to the algorithm, initially the unit matrix $Q = [D|A^T]$ is formed (Tab. 1, left). Next, the matrix is transformed, while the subsequent transitions are examined. In the presented example, only three transitions (out of six) are required to be processed to obtain the solution. Table 1 (right) shows the unit matrix after examination of the third transition. Note that four rows of $A^T$ are already zeroed. They refer to the place invariants formed in the matrix $D$ (marked by blue boxes). Clearly, those invariants cover all places in the net. The algorithm terminates its execution with the result that the system is bounded.

<figure><img src="image_3.png" /><figcaption>**Table 1.** Matrix $Q = [D|A^T]$ before the transformation (left) and after the transformation (right).</figcaption></figure>

# 5 Experiments

The proposed method was verified experimentally. Its effectiveness and efficiency was compared to the popular technique of place invariants computation (denoted as an *exact algorithm*), initially shown in [18]. Both methods were examined in terms of their runtime and obtained results (covering of the net by p-invariants). The set of
benchmarks includes 243 Petri nets, modelling real and hypothetical cyber-physical systems and control systems. Their description can be found on the websites: http://gres.uninova.pt and http://hippo.iee.uz.zgora.pl. The experiments were performed on the dedicated computational server: Intel® Xeon® Platinum 8160 @2.1 GHz processor, 16 GB of RAM. The results for selected benchmarks are shown in Tab. 2. The particular columns contain the following values: *Name of the system* – the name of the system described by a Petri net, |P| – the number of places, |T| – the number of transitions, *covered* – whether the system is covered by place invariants according to the algorithm, *runtime* – the execution time of the algorithm in milliseconds.

It can be observed that for small systems, containing a few places and transitions, (such as traffic\_light\_v2 or pn\_silva\_05e) both methods are efficient. It can be even noticed that the exact method computes the result faster than the proposed algorithm. However, in case of more complicated systems (such as ConsistentExample, crossroadSM\_FPGA), the difference is notable. The proposed method was able to compute the solution within a few seconds, while the runtime of the exact method is much longer (even more than 13 minutes in case of crossroadSM\_FPGA). Finally, a huge difference can be noticed in case of complex systems (zuberek5, cn\_crr7, cn\_crr25). For such systems, the exact method was not able to compute results due to the state explosion problem (the method was stopped after one hour, and denoted as “timeout” in the table). In contrast, the proposed method found the result for the worst case (cn\_crr25) in less than one and a half minute. Finally, let us note that module crossroadSM\_FPGA describes the real-life cyber-physical system (collision free crossroad for cars and pedestrians). It was implemented and partially reconfigured within the programmable device, thus the boundedness property was essential.

<table><caption>**Table 2.** Exemplary results of the experiments.</caption><thead><tr><th rowspan="2">Name of the system<br>(Petri net)</th><th rowspan="2">|P|</th><th rowspan="2">|T|</th><th colspan="2">exact method</th><th colspan="2">proposed method</th></tr><tr><th>covered</th><th>runtime<br>[ms]</th><th>covered</th><th>runtime<br>[ms]</th></tr></thead><tbody><tr><td>traffic\_light\_v2</td><td>4</td><td>3</td><td>Yes</td><td>0.424</td><td>Yes</td><td>0.415</td></tr><tr><td>pn\_silva\_05e</td><td>4</td><td>4</td><td>No</td><td>0.439</td><td>No</td><td>0.635</td></tr><tr><td>esparza2</td><td>15</td><td>13</td><td>Yes</td><td>3.366</td><td>Yes</td><td>1.061</td></tr><tr><td>2pusher</td><td>15</td><td>18</td><td>No</td><td>10.743</td><td>No</td><td>6.536</td></tr><tr><td>silva5</td><td>16</td><td>8</td><td>Yes</td><td>2.660</td><td>Yes</td><td>1.496</td></tr><tr><td>hulgaard1</td><td>19</td><td>12</td><td>Yes</td><td>27.805</td><td>Yes</td><td>3.275</td></tr><tr><td>ConsistentExample</td><td>29</td><td>26</td><td>No</td><td>42986.800</td><td>No</td><td>5752.120</td></tr><tr><td>zuberek1</td><td>30</td><td>22</td><td>Yes</td><td>22.324</td><td>Yes</td><td>3.273</td></tr><tr><td>crossroadSM\_FPGA</td><td>32</td><td>12</td><td>Yes</td><td>807879.000</td><td>Yes</td><td>183.985</td></tr><tr><td>zuberek5</td><td>41</td><td>31</td><td>n/a</td><td>timeout</td><td>Yes</td><td>45.045</td></tr><tr><td>cn\_crr7</td><td>56</td><td>15</td><td>n/a</td><td>timeout</td><td>Yes</td><td>155.278</td></tr><tr><td>cn\_crr25</td><td>200</td><td>51</td><td>n/a</td><td>timeout</td><td>Yes</td><td>78954.828</td></tr></tbody></table>

The performed experiments proved the effectiveness and efficiency of the proposed technique. The results obtained by both methods were the same for all examined benchmarks (for which the result for the exact method was obtained). This provides experimental validation of the correctness of the method. Furthermore, the runtime of the proposed method confirms its very high efficiency, since the result for the worst-case example was obtained in less than one and half a minute.
## 6 Conclusions

The design process of the control part of cyber-physical systems involves several aspects. One of them refers to the proper specification and further formal verification. In the paper an analysis technique of the boundedness property is proposed. The presented solution is based on the existing solutions and applies transformations of the incidence matrix of the system. Contrary to the other, most popular analysis techniques, the introduced method does not require computation of all place invariants in the system. The performed experiments proved its efficiency and effectiveness.

On the other hand, there is a limitation of the presented method. The boundedness of the Petri net is guaranteed only for those systems that are covered by place invariants. Otherwise, the system might be unbounded, but the final result remains unsolved. However, it should be underlined that such a situation (the net being bounded but not covered by place invariants) is rather rare (about 5.5% of the examined benchmarks). Nevertheless, this aspect is planned for further enhancement of the algorithm. Moreover, plans for future research include analysis of well-formed nets (safeness, liveness), which are the key properties of Petri net-based description of the control part of cyber-physical systems.

**Acknowledgments.** This work is supported by the National Science Centre, Poland, under Grant number 2019/35/B/ST6/01683.

## References

[1] C. Girault and R. Valk, *Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications*. Berlin Heidelberg: Springer-Verlag, 2003.

[2] A. Karatkevich, *Dynamic Analysis of Petri Net-Based Discrete Systems*. Berlin Heidelberg: Springer-Verlag, 2007.

[3] M. Zhou and N. Wu, *System Modeling and Control with Resource-Oriented Petri Nets*, 1 edition. Boca Raton, FL: CRC Press, 2009.

[4] T. Murata, "Petri nets: Properties, analysis and applications," *Proceedings of the IEEE*, vol. 77, no. 4, pp. 541–580, Apr. 1989, doi: 10.1109/5.24143.

[5] R. Wiśniewski, *Prototyping of Concurrent Control Systems Implemented in FPGA Devices*. Springer International Publishing, 2017.

[6] R. Wisniewski, M. Wisniewska, and M. Jarnut, "C-Exact Hypergraphs in Concurrency and Sequentiality Analyses of Cyber-Physical Systems Specified by Safe Petri Nets," *IEEE Access*, vol. 7, pp. 13510–13522, 2019, doi: 10.1109/ACCESS.2019.2893284.

[7] Z. Yu, L. Zhou, Z. Ma, and M. A. El-Meligy, "Trustworthiness Modeling and Analysis of Cyber-physical Manufacturing Systems," *IEEE Access*, vol. 5, pp. 26076–26085, 2017.

[8] I. Grobelna, R. Wiśniewski, and M. Wojnakowski, "Specification of Cyber-Physical Systems with the Application of Interpreted Nets," in *Proceedings of the IECON'19 - 45th Annual Conference of the IEEE Industrial Electronics Society*, Lisbon, Portugal, pp. 5887–5891.

[9] R. Wiśniewski, G. Bazydło, P. Szcześniak, and M. Wojnakowski, "Petri Net-Based Specification of Cyber-Physical Systems Oriented to Control Direct Matrix Converters With Space Vector Modulation," *IEEE Access*, vol. 7, pp. 23407–23420, 2019, doi: 10.1109/ACCESS.2019.2899316.
[10] E. A. Lee, "Cyber Physical Systems: Design Challenges," in *2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC)*, May 2008, pp. 363–369, doi: 10.1109/ISORC.2008.25.

[11] E. A. Lee and S. A. Seshia, *Introduction to Embedded Systems: A Cyber-Physical Systems Approach*, Second edition. Cambridge, Massachusetts: The MIT Press, 2016.

[12] N. Dey, A. S. Ashour, F. Shi, S. J. Fong, and J. M. R. S. Tavares, "Medical cyber-physical systems: A survey," *J Med Syst*, vol. 42, no. 4, p. 74, Mar. 2018, doi: 10.1007/s10916-018-0921-x.

[13] D. Jia, K. Lu, J. Wang, X. Zhang, and X. Shen, "A Survey on Platoon-Based Vehicular Cyber-Physical Systems," *IEEE Communications Surveys Tutorials*, vol. 18, no. 1, pp. 263–284, Firstquarter 2016, doi: 10.1109/COMST.2015.2410831.

[14] R. Wiśniewski, G. Bazydło, and P. Szcześniak, "Low-Cost FPGA Hardware Implementation of Matrix Converter Switch Control," *IEEE Transactions on Circuits and Systems II: Express Briefs*, vol. 66, no. 7, pp. 1177–1181, Jul. 2019, doi: 10.1109/TCSII.2018.2875589.

[15] R. Wiśniewski, A. Karatkevich, M. Adamski, A. Costa, and L. Gomes, "Prototyping of Concurrent Control Systems With Application of Petri Nets and Comparability Graphs," *IEEE Transactions on Control Systems Technology*, vol. 26, no. 2, pp. 575–586, Mar. 2018, doi: 10.1109/TCST.2017.2692204.

[16] J. Clempner, "An analytical method for well-formed workflow/Petri net verification of classical soundness," *International Journal of Applied Mathematics and Computer Science*, vol. 24, no. 4, pp. 931–939, Dec. 2014, doi: 10.2478/amcs-2014-0068.

[17] B. Li, M. Khlif-Bouassida, and A. Toguyéni, "On-The-Fly Diagnosability Analysis of Bounded and Unbounded Labeled Petri Nets Using Verifier Nets," *International Journal of Applied Mathematics and Computer Science*, vol. 28, no. 2, pp. 269–281, Jun. 2018, doi: 10.2478/amcs-2018-0019.

[18] J. Martínez and M. Silva, "A simple and Fast Algorithm to Obtain all Invariants of a Generalised Petri Net," in *Application and Theory of Petri Nets*, Berlin, Heidelberg, 1982, pp. 301–310, doi: 10.1007/978-3-642-68353-4_47.

[19] W. Reisig, "Nets Consisting of Places and Transistions," in *Petri Nets: An Introduction*, W. Reisig, Ed. Berlin, Heidelberg: Springer, 1985, pp. 62–76.

[20] J. R. Celaya, A. A. Desrochers, and R. J. Graves, "Modeling and analysis of multi-agent systems using petri nets," in *2007 IEEE International Conference on Systems, Man and Cybernetics*, Oct. 2007, pp. 1439–1444, doi: 10.1109/ICSMC.2007.4413960.

[21] G. K. H. Pang, R. Tang, and S. S. Woo, "Intelligent Control and Supervision Based on Fuzzy Petri Nets," in *Methods and Applications of Intelligent Control*, S. G. Tzafestas, Ed. Dordrecht: Springer Netherlands, 1997, pp. 217–243.

[22] S. Cang and H. Yu, "Overview of Modelling, Scheduling, Planning, and Control Using Petri Net Representation and AI Search," in *Advanced Design and Manufacture to Gain a Competitive Edge*, London, 2008, pp. 397–406, doi: 10.1007/978-1-84800-241-8_41.

[23] S. Edelkamp and S. Jabbar, "Action Planning for Directed Model Checking of Petri Nets," *Electronic Notes in Theoretical Computer Science*, vol. 149, no. 2, pp. 3–18, Feb. 2006, doi: 10.1016/j.entcs.2005.07.023.

[24] R. Wisniewski, M. Wojnakowski, and Ł. Stefanowicz, "Safety analysis of Petri nets based on the SM-cover computed with the linear algebra technique," *AIP Conference Proceedings*, vol. 2040, no. 1, p. 080008, Nov. 2018, doi: 10.1063/1.5079142.

[25] R. Wiśniewski, A. Karatkevich, Ł. Stefanowicz, and M. Wojnakowski, "Decomposition of distributed edge systems based on the Petri nets and linear algebra technique," *Journal of Systems Architecture*, vol. 96, pp. 20–31, Jun. 2019, doi: 10.1016/j.sysarc.2019.01.015.

[26] R. Zurawski and MengChu Zhou, "Petri nets and industrial applications: A tutorial," *IEEE Transactions on Industrial Electronics*, vol. 41, no. 6, pp. 567–583, Dec. 1994, doi: 10.1109/41.334574.