# Preliminary Verification of Liveness in a Control Part of Cyber-Physical Systems Modeled by a Petri Net

Mateusz Poplawski, Remigiusz Wiśniewski, Grzegorz Bazydlo, Maxim Maliński

► To cite this version:

Mateusz Poplawski, Remigiusz Wiśniewski, Grzegorz Bazydlo, Maxim Maliński. Preliminary Verification of Liveness in a Control Part of Cyber-Physical Systems Modeled by a Petri Net. 14th Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS), Jul 2023, Monte Da Caparica, Portugal. pp.205-215, 10.1007/978-3-031-36007-7_15 . hal-05473096

HAL Id: hal-05473096

https://inria.hal.science/hal-05473096v1

Submitted on 23 Jan 2026

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 CC BY 4.0 - Attribution - International License
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
<figure><img src="image_3.png" /></figure>

# Preliminary Verification of Liveness in a Control Part of Cyber-Physical Systems Modeled by a Petri Net

Mateusz Popławski<fnref n="1" />(✉), Remigiusz Wiśniewski<fnref n="1" />, Grzegorz Bazydło<fnref n="1" />, and Maxim Maliński<fnref n="2" />

**Abstract.** This paper proposes a novel approach for the liveness verification of a Petri net-based cyber-physical system (CPS). The idea is based on the reduction of the initial Petri net and further analysis of its structure in order to identify the sequences of places and transitions that may affect the liveness of the system. In particular, the technique searches for the sequences in the Petri net in order to determine whether the system may not be live, or, (in certain cases) it is definitely not live. The proposed method is mainly aimed at accelerating the process of initial verification of the control part of CPS. The main benefit of the presented technique is its polynomial computational complexity (the method runs in polynomial time). Therefore, the technique permits rapid checking of the system. Although this method is oriented toward CPSs, it can also be applied to other Petri net-based systems where liveness is especially important (e.g., concurrent control systems). The proposed technique was examined experimentally with a set of 242 benchmarks.

**Keywords:** Liveness · Control Part of the Cyber-Physical System · Petri Net

## 1 Introduction

Currently, on the market an increasing demand can be observed for new-generation systems, which combine the execution part (physical process) with cyber components. The behavior of such a system is defined by the physical part but also by the control (cyber) component. Such systems in the literature are called Cyber-Physical Systems (CPS) [1, 2]. CPSs are all around us: smart home automation devices [3], healthcare systems [4], power electronic converters [5], manufacturing systems [6], transportation systems [7], etc. CPSs permit to perform operations concurrently, which makes them possible to execute several operations at the same time [8]. The increasing number of components (as well as their complexity), and the growing use of advanced sensors and

<footnote n="1">¹ Institute of Control and Computation Engineering, University of Zielona Góra, 65-516 Zielona Góra, Poland
{m.poplawski,r.wisniewski,g.bazydło}@issi.uz.zgora.pl</footnote>

<footnote n="2">² University of Zielona Góra, 65-516 Zielona Góra, Poland
98881@g.elearn.uz.zgora.pl</footnote>
actuators cause a serious challenge related to the design and verification of modern CPS [9]. Petri nets [10] are one of the most efficient solutions for modeling and verification of CPSs [11], combining their graphical and readable notation with the intuitive expression of parallel behavior of the designed CPS [12]. Furthermore, their application in modeling of CPSs (or more generally – concurrent systems) has abounding benefits over other modeling techniques. The visualization of Petri nets using simple graphic elements (circles, rectangles, arrows) makes the models relatively readable and flexible. Moreover, well-developed verification techniques (e.g., invariants, reachability tree or graph analysis) allow for effective detection of most errors of CPS model [13, 14].

Petri nets are widely supported by several mathematical techniques. Therefore, the designer can perform the examination of the CPS at the early modelling stage. The main properties of a Petri net-based CPS are liveness, boundedness, and safeness [10]. Examination of those properties permits avoiding malfunctions of the modeled system, such as deadlocks, and redundant or unreachable states. The main problem with the traditional analysis techniques of a Petri net is exponential computational complexity, which makes their use in large and complex Petri nets extremely difficult. Therefore, it is worth developing methods that can simplify the analysis (unfortunately, the results may not be unambiguous, but from the other side they can indicate the path of further analysis).

The design of a CPS modelled by a Petri net consists of several stages, including modeling, verification, and analysis, as well as further hardware implementation [14, 15]. Petri net-based methods allow for the examination of the robustness and reliability of the CPS at the specification stage [16, 17], which may meaningly affect the costs and time and of the designed CPS. There are various verification techniques, including concurrency and sequentiality relations analysis, as well as Petri net properties examination, such as liveness, safeness and boundedness [12, 18–23]. Verification of such crucial attributes prevents deadlocks in the system and helps avoid redundancy (unreachable states) [24]. Unfortunately, verification and analysis of Petri net-based CPSs, especially liveness property, are not trivial tasks. The main bottleneck refers to the computational complexity of the existing algorithms. From one side, exact methods, such as those that apply the reachability tree/graph are effective and able to obtain optimal results. However, they do usually have exponential computational complexity, which means that the solution may never be found within the assumed time. On the other hand, the approximate algorithms are much more efficient (their run-time is executed within the assumed time), but the result may not be optimal. Therefore, there is very hard to find a comprehensive solution, and the existing techniques balance the optimal results (effectiveness) and reasonable computation time (efficiency) [15]. In the paper we propose a polynomial-time algorithm for preliminary liveness verification of the Petri net-based CPS. The main contributions are summarized as follows:

- a novel Petri net-based analysis technique is proposed, which allows the initial liveness examination of the model in order to determine whether the system *may not* be live, or, (in certain cases) it is *definitely not* live;

- a short computation time is the main benefit of the proposed solution;
- the presented technique was experimentally validated with a set of 242 benchmarks (test cases).

This paper is oriented on the preliminary liveness verification of a Petri net-based CPS (or more precisely the control part of CPS). After the initial reduction of the net [10], the defined sequences of places and transitions are searched in the system. In particular, the method determines whether the given net may be dead and in special cases shows lack of liveness. Let us underline that this paper is focused on the control part of CPSs. In opposite to the traditional concurrent systems, the control part of the CPS (also called the “cyber part”) is strictly joined with the “physical” (execution) part. Such a combination can be observed in other works published by authors, including manufacturing systems [6], integrated systems [5, 25], and distributed systems [26]. However, in our previous papers, boundedness and safeness analysis was emphasized [27]. This paper deals with the liveness examination of the control part of CPS.

The rest of the paper is structured as follows. Section 2 presents the relation of the presented research with technological innovation for connected cyber-physical spaces. Section 3 introduces the necessary definitions and notations. The idea of the proposed technique is presented in Sect. 4. Section 5 presents the experimental results of the proposed method, and the final conclusion can be found in Sect. 6.

## 2 Technological Innovation for Connected Cyber-Physical Spaces

The continuous technological development in recent years, additionally intensified by the coronavirus pandemic [28], has meant that our current environment is now filled with various types of *smart* systems and electronic services. We live in *smart* cities, in *smart* buildings, controlled by *smart* home systems. We watch *smart* TV and use *smartphones*. We are a *smart* society [29]. We are increasingly using artificial intelligence systems to make our lives safer, more convenient, cheaper, and more efficient. Many people cannot imagine functioning in everyday life without using electronic devices or smart gadgets.

We live in environments, where both physical and cyber spaces intersect. Nowadays, we are encompassed by countless CPSs. In addition, present-day CPSs are anticipated to be viably securing personal information, energy effective, small in size, valuable, effec- tively versatile, and secure. In particular, the last mentioned prerequisite is requesting since these days CPS are complex, progressive, and exceptionally regularly concurrent. The possibility of making a mistake by designing such complex systems is natural and large. Removal of such errors revealed only in the implementation phase can be very expensive. Moreover, unrelated errors can be dangerous for people (think about defective medical devices). Therefore, there is an urgent need for the development of methods and techniques which can analyze the model in the first stages of the CPS design process. Petri nets are one of the promising modeling techniques because they are simple and effective. Moreover, they are supported by a set of methods for model analysis (e.g., invariants, reachability tree analysis, deadlock search) that allow for the detection of the design errors at the model stage.

The analysis technique proposed in the paper is oriented on the preliminary liveness verification of a Petri net-based CPS (more precisely, the control part of CPS). The presented method, after the initial reduction of the Petri net, analyzes the model in order
to find the particular sequences of places and transitions. Finally, the method determines whether the Petri net is not live. Such an approach fits into the current trend of developing systems that are smarter with increasing levels of cognition and autonomy, oriented to solve societal problems with a human-centric perspective.

## 3 Main Definitions, Notations, and Reduction Techniques

This section presents the main definitions and notations for better clarification of the proposed method [10, 12, 13, 15, 17–19, 21–23]. Moreover, it also briefly introduces the reduction techniques applied in the proposed approach.

**Definition 1** (Petri net). A Petri net $N$ is a 4-tuple – Eq. (1):

$$N = (P, T, F, M_0) \qquad (1)$$

where $P$ is a finite set of places, $T$ is a finite set of transitions, $F \subset (P \times T) \cup (T \times P)$ is a finite set of arcs, $M_0$ is an initial marking.

**Definition 2** (Input (output) places (transitions)). Sets of input and output places of a transition are defined respectively as follows: $\bullet t = \{p \in P : (p, t) \in F\}$, $t \bullet = \{p \in P : (t, p) \in F\}$. The sets of input and output transitions of a place are defined: $\bullet p = \{t \in T : (t, p) \in F\}$, $p \bullet = \{p \in P : (p, t) \in F\}$.

**Definition 3** (Marking). A marking (state) $M$ of a Petri net is a distribution of tokens in the net places. If a place contains one or more tokens, it is called a marked place. A marking can be changed by means of firing (execution) of a transition.

**Definition 4** (Firing). A transition $t$ is enabled and can fire (be executed), if every of its input places contains a token. Transition firing removes one token from each input place and adds one token to each output place.

**Definition 5** (Reachability). Marking $M_j$ is reachable from marking $M_i$, if $M_i$ can be changed to $M_j$ by a sequence of transition firings.

**Definition 6** (Incidence matrix). Matrix $A_{m \times n}$ is an incidence matrix of a Petri net $N = (P, T, F, M_0)$ with $|P|$ columns and $|T|$ rows of integers, given by – Eq. (2):

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

**Definition 7** (Liveness). Petri net $N$ is live if it is possible to fire any transition from any reachable marking by a sequence of firings of other transitions.
Please note that the above definition refers to the strictest condition of liveness. There exist also other liveness definitions, which are more relax (denoted by “liveness levels”), cf. [10].

Finally, let us present the reduction techniques applied in the paper. Reduction techniques allows for the simplification of the Petri net structure [9]. It is worth mentioning that such operations preserve the main properties of the analyzed system, including liveness. In general, the reductions can be divided into four groups: Fusion of Series Places (FSP) (Fig. 1a), Fusion of Series Transitions (FST) (Fig. 1b), Fusion of Parallel Places (FPP) (Fig. 1c), Fusion of Parallel Transitions (FPT) (Fig. 1d). Let us briefly describe them.

The first reduction method (FSP) combines places that are modeled as a sequence. There is a restriction in regard to the places that are initially marked (with tokens), which cannot be reduced (Fig. 1a). Similarly, the FST reduction is executed. This technique also has a restriction, thus the places initially marked cannot be reduced (Fig. 1b). Third reduction method (FPP) is based on the elimination of the places that are modeled as parallelly. The method can be applied if each of reduced places contains a token, or none of them contains a token (Fig. 1c). Finally, the FPT is executed in the similar way. However, in this case, there are no restrictions on marked places (Fig. 1d).

<figure><img src="image_4.png" /><figcaption>Fig. 1. Reduction techniques: FSP (a), FST (b), FPP (c), and FPT (d)</figcaption></figure>
## 4 The Idea of the Proposed Technique

This section presents the proposed liveness verification technique of the control part of CPS. The system is initially reduced with the set of techniques presented within Sect. 3 (Fig. 1). In the proposed liveness verification technique, the above four methods are executed periodically until there is a possibility for further reductions. The main aim of the applied reductions is simplification of the Petri net structure with preservation of the liveness property. Such reductions influence on the second part of the proposed technique, since the specific sequences may be detected in easier way.

The main idea of the proposed technique refers to the searching of the certain sequences of places and transitions in the system. The presented methods are divided into two main groups. The algorithms presented in the first group indicate that the system *may not* be live. This means that the Petri net contains sequences of places that may lead to e.g., deadlock or not reachable states, but we are not sure about it. Therefore, the designer ought to perform additional verification or validation (simulation) of the system. In opposite, detection of the second group of sequences indicates that the Petri net is definitely not live. Hence, no further examinations are required.

The first group consists of four types of sequences, as shown in Fig. 2. The first case (most from the left) consists of three transitions and a single marked place. The second sequence (the next from the left) is structurally the same as the first one, but it does not contain a token. The third sequence includes three transitions and two marked places. Finally, the last sequence consists of four transitions, and two places, while one of them is marked. Indication of the above sequences indicate that the system *may not* be live. This means that if a particular sequence occurs in the Petri net, the designer should carefully examine the proper functionality of the CPS.

<figure><img src="image_5.png" /><figcaption>Fig. 2. Sequences indicating that the system *may not* be live</figcaption></figure>
The second group of sequences includes two cases, as shown in Fig. 3. Existence of each of them assures that the examined Petri net is not live. The first case (shown in Fig. 3 on the left) consists of a marked place (with a token), and a transition. Similarly, the second sequence contains a place (but without a token), and a transition.

<figure><img src="image_6.png" /><figcaption>Fig. 3. Sequences indicating that the system is not live</figcaption></figure>

Let us now present the technique that permit to find the above cases. The method that detects sequences from both first group is divided into two main steps. Firstly, the algorithm checks the occurrence of the sequences from the first group: first, second, and third cases (Fig. 2a, 2b, 2c). Subsequently, the fourth case from the first group is investigated (Fig. 2d), moreover, the algorithm searches for the sequences from the second group (Fig. 3). As the input, the algorithm reads the incidence matrix of a Petri net (after reductions). Existence of the above sequences indicates that the system is definitely not live. This means that no further examinations are required and the Petri net ought to be revised (re-modelled). It should be noted that the designer is able to locate the improper areas of the Petri net (detected by the proposed algorithm).

Moving into details the algorithm comprises the following stages:

1. For each transition $t$:

a) if ($|\bullet t| = 1$ and $|t\bullet| = 1$) then:

- if $|t \bullet \bullet| = 2$ and $|t\bullet|$ is marked then the Petri net contains a sequence from the first group, first case (shown in Fig. 2a);

- if $|t \bullet \bullet| = 2$ and $|t\bullet|$ is not marked then the Petri net contains a sequence from the first group, second case (shown in Fig. 2b);

b) if ($|\bullet t| = 1$ and $|t\bullet| = 2$) then:

- if both output places $p_1$ and $p_2$ of $t$ are marked and additionally ($|p_1\bullet| = 2$ and $|p_2\bullet| = 1$) such that $(p_2\bullet) = (p_1\bullet)$ then the Petri net contains a sequence from the first group, third case (Fig. 2c);

2. For each place $p$:

a) if ($|\bullet p| = 2$ and $|p\bullet| = 2$ and $p$ is marked) then:

- if there exists ($p' = p \bullet \bullet$) such that $[(p\bullet) = (p'\bullet)]$ and $[(p'\bullet) = (\bullet p)]$ and ($|\bullet p'| = |p'\bullet| = 1$) then the Petri net contains a sequence from the first group, fourth case (shown in Fig. 2d);
b) if ($|\bullet p| = 0$) and $|p\bullet| = 1$ then:

- if *p* is marked then the Petri net contains a sequence from the second group, first case (shown in Fig. 3a);

- if *p* is not marked then the Petri net contains a sequence from the second group, second case (shown in Fig. 3b).

As already mentioned, the occurrence of sequences from the first group indicates that the system *may not* be live. However, if the sequence from the second group is detected then the Petri net is definitely not live.

# 5 Results of Experiments

In this part, the results of experimental research will be presented and discussed. The proposed technique was examined in terms of its efficiency (run-time) and effectiveness (proper results). The method was tested on the dedicated laptop with the use of an Intel® Core® i7-1165G7@2.8 GHz processor and 32 GB of RAM. The set of benchmarks contains 242 Petri nets that describe theoretical and real-life CPSs, control systems, manufacturing systems, discrete systems, etc. The tests are available at: http://www.hippo.uz.zgora.pl.

<table><caption>**Table 1.** Results of the experiments for selected benchmarks.</caption><thead><tr><th rowspan="2">Benchmark name</th><th colspan="2">Number of places in the context of reduction</th><th colspan="2">Number of transitions in the context of reduction</th><th colspan="2">1<sup>st</sup> Group of sequences</th><th colspan="2">2<sup>nd</sup> Group of sequences</th><th colspan="2">Reachability graph</th></tr><tr><th>pre</th><th>after</th><th>pre</th><th>after</th><th>Result</th><th>Runtime [ms]</th><th>Result</th><th>Runtime [ms]</th><th>Result</th><th>Runtime [ms]</th></tr></thead><tbody><tr><td>CNC_machine</td><td>7</td><td>5</td><td>2</td><td>1</td><td>Not occurs</td><td>0,016</td><td>Not live</td><td>0,013</td><td>Not live</td><td>21,241</td></tr><tr><td>tank_heating</td><td>4</td><td>4</td><td>2</td><td>1</td><td>Not occurs</td><td>0,014</td><td>Not live</td><td>0,012</td><td>Not live</td><td>121,881</td></tr><tr><td>lnet_p8n1</td><td>51</td><td>40</td><td>3</td><td>2</td><td>Not occurs</td><td>0,024</td><td>Not live</td><td>0,018</td><td>Not live</td><td>44192,545</td></tr><tr><td>s_net_copy_milling_machine_subprocess</td><td>31</td><td>28</td><td>5</td><td>6</td><td>Potentially not live</td><td>0,167</td><td>Not occurs</td><td>0,086</td><td>Not live</td><td>697,037</td></tr><tr><td>bause1</td><td>11</td><td>11</td><td>9</td><td>9</td><td>Potentially not live</td><td>0,978</td><td>Not occurs</td><td>0,319</td><td>Not live</td><td>44,087</td></tr><tr><td>balduzzi1</td><td>18</td><td>16</td><td>18</td><td>16</td><td>Potentially not live</td><td>13,862</td><td>Not occurs</td><td>2,820</td><td>Not live</td><td>31,324</td></tr><tr><td>esparza1</td><td>11</td><td>10</td><td>10</td><td>9</td><td>Potentially not live</td><td>0,537</td><td>Not occurs</td><td>0,261</td><td>Not live</td><td>94,952</td></tr></tbody></table>

Table 1 shows the experimental results for the selected benchmarks. The obtained results of these tests were compared to a full liveness analysis using the state reachability graph [10]. In the “Benchmark” column are the names of the analyzed systems. The next
two columns show the number of places and transitions before and after the reduction. The result of the first group of sequences was denoted either by “potentially not live” (if the sequence was detected) or “not occurs” (in another case). The result of the second group “not live” indicates that the sequence was found, while the opposite case is denoted by “not occurs”.

The experiments show that the presented approach has potential. The time of the proposed method is shorter than the reference method used for comparison. It should be emphasized that the occurrence of sequences from the first group means that the system *may not* be live (but it does not have to be). The occurrence of sequences from the second group means that the tested Petri Net is definitely not live. Going into detail, the sequence from the first group was found in 36 systems, while 17 of them were indeed not live. This means that 47% of detected Petri nets were not live. Let us underline that this is relatively high result, since almost half of the indicated systems contain errors, which are usually very hard to detect (the traditional methods based on the reachability tree/graph are often insufficient due to the exponential computational complexity). Moving on to the second group of sequences, they were found in 18 tested cases. It should be noted that all of them were indeed not live. This means that the experimental results fully confirmed the theoretical expectations.

# 6 Conclusions

A method of preliminary liveness verification of Petri net-based CPSs was proposed in the paper. The technique includes the initial reduction of the Petri net, and further searching for the particular sequences of places and transitions in the system. Two kinds of such sequences are proposed and analyzed. The occurrence of the first of them indicates that the system *may not* be live. Furthermore, existence of the second group of sequences assures that the Petri net is not live.

The experimental results confirm the efficiency and effectiveness of the proposed method. The sequences from the first group were obtained for 36 Petri nets (out of 242 analyzed), while 17 of them are indeed not live. Furthermore, 18 systems contain the sequences from the second group, and all of them were not live. On the other hand, there are limitations of the proposed algorithm. First of all, the method is oriented on the preliminary verification of the system, thus it is not able to indicate all Petri nets that are not live. Furthermore, detection of a sequence from the first group requires additional analysis. Even if such a sequence is detected, it does not mean that the system is not live, and further verification/validation is required. However, let us point out, that such an analysis is very fast (confirmed by experimental results). Moreover, such an information can be extremely useful, especially in the case of relatively large CPS.

Future work includes further development of the proposed technique. Firstly, the proposed ideas are going to be proved formally, including their functionality, as well as computational complexity. Moreover, it is planned to include linear algebra techniques in order to combine the presented method with boundedness verification and deadlocks detection.

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

1. Ryalat, M., ElMoaqet, H., AlFaouri, M.: Design of a smart factory based on cyber-physical systems and Internet of Things towards Industry 4.0. Appl. Sci. **13**, 2156 (2023). https://doi.org/10.3390/app13042156

2. Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems: A Cyber-Physical Systems Approach. MIT Press, Cambridge (2017)

3. Shih, C.-S., Chou, J.-J., Reijers, N., Kuo, T.-W.: Designing CPS/IoT applications for smart buildings and cities. IET Cyber-Phys. Syst. Theory Appl. **1**, 3–12 (2016). https://doi.org/10.1049/iet-cps.2016.0025

4. Dey, N., Ashour, A.S., Shi, F., Fong, S.J., Tavares, J.M.R.S.: Medical cyber-physical systems: a survey. J. Med. Syst. **42**, 74 (2018). https://doi.org/10.1007/s10916-018-0921-x

5. Wiśniewski, R., Bazydło, G., Szcześniak, P.: Low-cost FPGA hardware implementation of matrix converter switch control. IEEE Trans. Circ. Syst. II Express Briefs **66**, 1177–1181 (2019). https://doi.org/10.1109/TCSII.2018.2875589

6. Patalas-Maliszewska, J., Posdzich, M., Skrzpek, K.: Modelling Information for the bur- nishing process in a cyber–physical production system. Int. J. Appl. Math. Comput. Sci. **32**, 345–354 (2022). https://doi.org/10.34768/amcs-2022-0025

7. Guo, Y., Hu, X., Hu, B., Cheng, J., Zhou, M., Kwok, R.Y.K.: Mobile cyber physical systems: current challenges and future networking applications. IEEE Access **6**, 12360–12368 (2018). https://doi.org/10.1109/ACCESS.2017.2782881

8. Lee, E.A.: Cyber physical systems: design challenges. In: 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC), pp. 363–369 (2008). https://doi.org/10.1109/ISORC.2008.25

9. Wiśniewski, R., Wojnakowski, M., Li, Z.: Design and verification of Petri-net-based cyber-physical systems oriented toward implementation in field-programmable gate arrays—a case study example. Energies **16**, 67 (2023). https://doi.org/10.3390/en16010067

10. Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE **77**, 541–580 (1989). https://doi.org/10.1109/5.24143

11. Liu, Z., Hu, L., Hu, W., Tan, J.: Petri nets-based modeling solution for cyber-physical product control considering scheduling, deployment, and data-driven monitoring. IEEE Trans. Syst. Man Cybern. Syst. **53**, 990–1002 (2023). https://doi.org/10.1109/TSMC.2022.3170489

12. Wojnakowski, M., Wiśniewski, R., Bazydło, G., Popławski, M.: Analysis of safeness in a Petri net-based specification of the control part of cyber-physical systems. Int. J. Appl. Math. Comput. Sci. **31**, 647–657 (2021). https://doi.org/10.34768/amcs-2021-0045

13. Girault, C., Valk, R.: Petri Nets for Systems Engineering. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-662-05324-9

14. Wiśniewski, R., Bazydło, G., Gomes, L., Costa, A., Wojnakowski, M.: Analysis and design automation of cyber-physical system with hippo and IOPT-tools. In: IECON 2019 - 45th Annual Conference of the IEEE Industrial Electronics Society, Lisbon, Portugal, pp. 5843–5848. IEEE Press (2019). https://doi.org/10.1109/IECON.2019.8926692

15. Wiśniewski, R.: Prototyping of Concurrent Control Systems Implemented in FPGA Devices. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-45811-3

16. Li, B., Khlif-Bouassida, M., Toguyéni, A.: On–the–fly diagnosability analysis of bounded and unbounded labeled Petri nets using verifier nets. Int. J. Appl. Math. Comput. Sci. **28**, 269–281 (2018). https://doi.org/10.2478/amcs-2018-0019

17. Karatkevich, A.: Dynamic Analysis of Petri Net-Based Discrete Systems. Springer, Heidel- berg (2007). https://doi.org/10.1007/978-3-540-71560-3

18. Best, E., Devillers, R., Koutny, M.: Petri Net Algebra. Springer, Heidelberg (2001). https://doi.org/10.1007/978-3-662-04457-5
19. David, R., Alla, H.: Bases of petri nets. In: David, R., Alla, H. (eds.) Discrete, Continuous, and Hybrid Petri Nets, pp. 1–20. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-10669-9_1

20. Wojnakowski, M., Wiśniewski, R.: Verification of the boundedness property in a Petri net-based specification of the control part of cyber-physical systems. In: Camarinha-Matos, L.M., Ferreira, P., Brito, G. (eds.) DoCEIS 2021. IAICT, vol. 626, pp. 83–91. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-78288-7_8

21. Silva, M., Colom, J.M., Campos, J.: Linear algebraic techniques for the analysis of Petri nets. In: Recent Advances in Mathematical Theory of Systems, Control, Networks, and Signal Processing II, Tokyo, Japan, pp. 35–42. Mita Press (1992)

22. Esparza, J., Silva, M.: A polynomial-time algorithm to decide liveness of bounded free choice nets. Theor. Comput. Sci. **102**, 185–205 (1992). https://doi.org/10.1016/0304-3975(92)90299-0

23. Barkaoui, K., Minoux, M.: A polynomial-time graph algorithm to decide liveness of some basic classes of bounded Petri nets. In: Jensen, K. (ed.) ICATPN 1992. LNCS, vol. 616, pp. 62–75. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55676-1_4

24. Guo, X., Wang, S., You, D., Li, Z., Jiang, X.: A siphon-based deadlock prevention strategy for S³PR. IEEE Access **7**, 86863–86873 (2019). https://doi.org/10.1109/ACCESS.2019.2920677

25. Wiśniewski, R., Bazydło, G., Szcześniak, P., Wojnakowski, M.: Petri net-based specification of cyber-physical systems oriented to control direct matrix converters with space vector modulation. IEEE Access **7**, 23407–23420 (2019). https://doi.org/10.1109/ACCESS.2019.2899316

26. Grobelna, I., Wiśniewski, R., Grobelny, M., Wiśniewska, M.: Design and verification of real-life processes with application of Petri nets. IEEE Trans. Syst. Man Cybern. Syst. **47**, 2856–2869 (2017). https://doi.org/10.1109/TSMC.2016.2531673

27. Wojnakowski, M., Popławski, M., Wiśniewski, R., Bazydło, G.: Hippo-CPS: verification of boundedness, safeness and liveness of Petri net-based cyber-physical systems. In: Camarinha-Matos, L.M. (ed.) Technological Innovation for Digitalization and Virtualization, pp. 74–82. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-07520-9_7

28. He, W., Zhang(Justin), Z., Li, W.: Information technology solutions, challenges, and suggestions for tackling the COVID-19 pandemic. Int. J. Inf. Manag. **57**, 102287 (2021). https://doi.org/10.1016/j.ijinfomgt.2020.102287

29. Foresti, R., Rossi, S., Magnani, M., Guarino Lo Bianco, C., Delmonte, N.: Smart society and artificial intelligence: big data scheduling and the global standard method applied to smart maintenance. Engineering **6**, 835–846 (2020). https://doi.org/10.1016/j.eng.2019.11.014