Necessary and sufficient liveness condition of GS³PR Petri nets

Abstract

Structural analysis is one of the most important and efficient methods to investigate the behaviour of Petri nets. Liveness is a significant behavioural property of Petri nets. Siphons, as structural objects of a Petri net, are closely related to its liveness. Many deadlock control policies for flexible manufacturing systems (FMS) modelled by Petri nets are implemented via siphon control. Most of the existing methods design liveness-enforcing supervisors by adding control places for siphons based on their controllability conditions. To compute a liveness-enforcing supervisor with as much as permissive behaviour, it is both theoretically and practically significant to find an exact controllability condition for siphons. However, the existing conditions, max, max′, and max″-controllability of siphons are all overly restrictive and generally sufficient only. This paper develops a new condition called max*-controllability of the siphons in generalised systems of simple sequential processes with resources (GS³PR), which are a net subclass that can model many real-world automated manufacturing systems. We show that a GS³PR is live if all its strict minimal siphons (SMS) are max*-controlled. Compared with the existing conditions, i.e., max-, max′-, and max″-controllability of siphons, max*-controllability of the SMS is not only sufficient but also necessary. An example is used to illustrate the proposed method.

Keywords:

• Petri net
• liveness
• siphon
• controllability condition

Acknowledgements

This work was supported in part by the Natural Science Foundation of China under Grant No. 61074035 and the Fundamental Research Funds for the Central Universities under Grant No. K5051204009.

Notes

The resources in flexible manufacturing systems are conservative. A resource has a capacity of processing units that are represented by the tokens in a place that models the resource. A resource is either idle, implying that there is no ongoing processing stage that needs it, or some or all units are occupied by processing stages. In the context of a Petri net model, the tokens initially marked in a resource place are either in the resource place or in the operation places that need the resource to support.

A deadlock prevention policy is said to be conservative if its resulting supervisor excludes some legal states, which implies that the supervisor is not maximally permissive.

The concept of circular waits in Petri nets are presented in Jeng (1997), Lewis, Gürel, Bogdan, Doanalp, and Pastravanu (1998), and Liu, Li, and Zhou (2010b). For any two r_i, r_j ∈ P_R, r_i is said to wait for r_j, denoted as r_i → r_j, if the availability of r_j is an immediate requirement for the release of r_i, or equivalently, if ∃t ∈ ^•r_i∩r^•_j. An R-path between r_i and r_k is defined as a set of resource places such that r_i → r_j → ⋅⋅⋅ → r_k. Then r_i is said to wait over an R-path for r_k, denoted as r_i↪r_k, if there is an R-path between r_i and r_k (Liu et al. 2010b). A circular wait is a set of resource places C ⊆ P_R, with |C| > 1, such that for any ordered pair {r_i, r_j} ⊆ C, r_i↪r_j (Lewis et al. 1998).

Additional information

Notes on contributors

GaiYun Liu

GaiYun Liu received the BS and PhD degrees from Xidian University, Xi'an, China, in 2006 and 2011, respectively. Since 2011, she has been with Xidian University, where she is currently a lecturer with the School of Electro-Mechanical Engineering. Her research interests include Petri net theory and applications and supervisory control of discrete event systems.

Kamel Barkaoui

Kamel Barkaoui is a professor of computer science at the Conservatoire National des Arts et Métiers (CNAM-Paris). He obtained the PhD (1988) and Habilitation à Diriger des Recherches (1998) in computer science from Université Paris 6 (UPMC). His research interests include formal methods for verification, control and performance evaluation of concurrent and distributed systems. He published over 90 refereed international journal articles and conference papers and received the IEEE International Conference on System, Man, and Cybernetics Outstanding Paper Award in 1995. He has served as programme committees and as programme committee chairs and organising chairs for numerous international workshops and conferences. He was a guest editor of Journal of Systems and Software (JSS) and International Journal of Critical Computer-Based Systems (IJCCBS).