Many deadlock control methods rely on reachability graphs of Petri nets (PN), thus suffering from state-space explosion issues. This paper proposes a novel approach to designing liveness-enforcing supervisors for PN by constructing its maximally good step graphs (MGSG), a class of partial order techniques in mitigating the aforementioned issues. Specifically, we first categorize the MGSG markings into allowed and unallowed ones. Then, we define good and risky transitions at allowed markings. Through the execution of risky transitions, the initial marking cannot be reachable from the allowed ones. Next, we design a maximal number of risky transitions (MNRT) problem to compute control places. In MNRT, all allowed markings and the firing of all good transitions are permitted, while risky transitions are forbidden. The objective is to maximize the prevention of risky transitions by using a single control place, which can be achieved by solving an integer linear programming problem. MNRT problems are recursively solved for unforbidden risky transitions until their resulting markings are prohibited. Finally, a controlled PN is generated and has been demonstrated to retain liveness. The experimental results show that our approach effectively reduces the number of control places and mitigates state-space explosion issues over its state-of-the-art peers. Note to Practitioners—Raw materials are handled in manufacturing systems through a series of well-coordinated processes. However, multiple processes competing for the same resources (like machines or robots) may result in an undesirable deadlock situation, where production slows down or entirely halts. A liveness-enforcing supervisor is designed to counter such a situation. As a mathematical tool, PN can be applied to model manufacturing systems. The supervisor design involves adding control places and directed arcs into PN to ensure its liveness, which implies that the systems can execute their tasks and never enter into deadlocks. In this work, we develop a deadlock control approach, which can generate a live and controlled PN without exploring a complete state space of PN. Experimental results show the effectiveness of our approach in reducing the number of control places and its practicability applied to large-scale systems, thus surpassing state-of-the-art methods.

Automated chromosome instance segmentation from metaphase cell microscopic images is critical for the diagnosis of chromosomal disorders (i.e., karyotype analysis). However, it is still a challenging task due to lacking of densely annotated datasets and the complicated morphologies of chromosomes, e.g., dense distribution, arbitrary orientations, and wide range of lengths. To facilitate the development of this area, we take a big step forward and manually construct a large-scale densely annotated dataset named AutoKary2022, which contains over 27,000 chromosome instances in 612 microscopic images from 50 patients. Specifically, each instance is annotated with a polygonal mask and a class label to assist in precise chromosome detection and segmentation. On top of it, we systematically investigate representative methods on this dataset and obtain a number of interesting findings, which helps us have a deeper understanding of the fundamental problems in chromosome instance segmentation. We hope this dataset could advance research towards medical understanding. The dataset can be available at:https://github.com/wangjuncongyu/chromosome-instance-segmentation-dataset.

Resource allocation systems (RASs) exist in various fields of modern society. The deadlock control problem is a crucial issue in control theory of RAS. This work is concentrated on a special class of shared resource and process-oriented Petri nets whose initial marking can have only a token in every resource place. Using mixed-integer programming (MIP) and iterative siphon control, we present a two-stage deadlock prevention policy. In particular, a modified MIP technique is developed for the first stage to compute a specific type of emptiable siphons and a siphon control method introducing monitors with related arcs whose weights all equal to one is established in the second stage. This policy leads to a maximally permissive liveness-enforcing supervisor and such an obtained controlled net is ordinary. Moreover, it avoids the exhaustive enumeration of siphons and the reachability analysis. Examples are provided to explain the policy.

Wire rod and bar rolling is an important batch production process in steel production systems. A scheduling problem originated from this process is studied in this work by considering the constraints on sequence-dependent family setup time and release time. For each serial batch to be scheduled, it contains several jobs and the number of late jobs within it varies with its start time. First, we model a rolling process using a Petri net (PN), where a so-called rolling transition describes a rolling operation of a batch. The objective of the concerned problem is to determine a firing sequence of all rolling transitions such that the total number of late jobs is minimal. Next, a mixed-integer linear program is formulated based on the PN model. Due to the NP-hardness of the concerned problem, iterated greedy algorithm (IGA)-based methods by using different neighborhood structures and integrating a variable neighborhood descent method are developed to obtain its near-optimal solutions. To test the accuracy, speed, and stability of the proposed algorithms, we compare their solutions of different-size instances with those of CPLEX (a commercial software) and four heuristic peers. The results indicate that the proposed algorithms outperform their peers and have great potential to be applied to industrial production process scheduling.Note to Practitioners—This work deals with a scheduling problem of a batch production process, i.e., wire rod and bar rolling, which is modeled by a Petri net (PN). Due to the NP-hardness of the concerned problem, four iterated greedy algorithm-based methods are developed to solve it. The proposed methods are validated and tested by comparing their solutions with those of four heuristic peers and the exact ones (when available via CPLEX). Extensive experimental results show that they can fast solve one-week-scale instances with better performance than their peers’, thereby proving the readiness to put them in industrial use. When solving a one-month-scale instance, the proposed methods show much better performance than others.

In cyber–physical systems (CPSs), it is of great importance to handle network attack issues. In this article, we consider the supervisory control layer of CPSs, focusing on closed-loop control systems vulnerable to sensor-reading modification attacks (SM-attacks), which may disguise the occurrence of an event as a different event by modifying appropriately sensor readings in sensor communication channels. In particular, we consider the plant modeled as a bounded Petri net and the control specification consisting in liveness enforcing. Based on repeatedly computing a more restrictive liveness-enforcing supervisor under no attack and constructing a so-called basic supervisor, a method that synthesizes a liveness-enforcing supervisor tolerant to an SM-attack is proposed.

This work focuses on a class of Petri nets (PNs) called Weighted Systems of Simple Sequential Processes with Resources (WS3PR). We study how to enforce liveness to WS3PR by appropriately allocating resources. A sufficient condition that guarantees liveness of a net system in this class is first derived. Then, based on such a condition, we propose an algorithm that computes an initial marking of resource places that guarantees the liveness of a WS3PR system where the initial marking of the idle places is given. Note that, we do not guarantee that the resulting solution is optimal, in the sense that a smaller initial marking of resource places that still leads to liveness could exist. However, several numerical examples show that the solution resulting from the proposed approach is optimal.

The main contribution of this correspondence paper consists in a linear algebraic characterization of the admissible marking set relative to a Petri net with uncontrollable transitions, subject to a linear constraint. In more detail, given a linear constraint that limits the number of tokens in one place, an algorithm is proposed to compute an approximation of the admissible marking set in terms of a disjunction of transformed linear constraints. The optimality of the solution is guaranteed provided that certain conditions are satisfied during the intermediate steps of the iterative approach. In all the other cases, the set of markings described by the transformed constraints could be surely contained in the admissible marking set.

The efficient siphon computation is the key to the development of siphon-based deadlock control strategies with good performance. This work studies the computation of minimal siphons in a class of Petri nets called S4PR. Firstly, we propose a function with polynomial complexity to determine whether a resource subset can generate a minimal siphon. Next, using the technique of problem partitioning, a new approach is developed to compute all minimal siphons in S4PR. Finally, an example is given to illustrate the proposed approach.

Deadlock prevention policies for flexible manufacturing systems (FMS) usually suffer from redundant monitors since some monitors may be added to the siphons that are originally controlled. To eliminate these redundant monitors, the controllability condition of siphons is studied in this work. For a class of Petri nets called Systems of Simple Sequential Processes with Resources (S3PR), new concepts of simple and complex strict minimal siphons (SMS) are introduced. More importantly, a necessary and sufficient condition of controllability of complex SMS is proposed for the first time. Based on this condition, an algorithm is given to control all SMS via M-controlling part of them and a structurally simple optimal liveness-enforcing supervisor can thus be synthesized for some classes of S3PR. Two examples are provided to illustrate the application of the proposed algorithm and show its superiority to prior work.

Reachability is an important dynamic property of Petri nets. Its determination given an unbounded net and initial marking has remained an open problem since 1960s. Due to its extreme difficulty, a great deal of research has been focused on some subclasses of unbounded nets. For arbitrary ones, this work intends to propose a new reachability tree (NRT), which consists of only but all reachable markings from its initial marking. Furthermore, an NRT-based method to decide deadlocks of unbounded nets is presented. An example is provided to show the new results.

Deadlocks are a rather undesirable phenomenon in flexible manufacturing systems (FMSs). This work, by adding monitors, develops a deadlock prevention policy for FMSs that can be modeled by a class of Petri nets called α-S3PR with i-resources. First, an algorithm is presented to reduce an S3PR via a i-resource. Based on the algorithm, i-resources in α-S3PRs are classified into two types: 1) A-ξ-resources and 2) B-ξ-resources. Next, for an α-S3PR with only B-ξ-resources, it is proved that a maximally permissive liveness-enforcing supervisor can be designed by controlling all emptied strict minimal siphons. For an α-S3PR containing A-ξ-resources, a liveness-enforcing supervisor can be designed by iteratively reducing the net via A-ξ-resources and adding the corresponding monitors. Finally, a deadlock prevention algorithm for α-S3PRs is presented. Two FMS examples are used to illustrate its application. Its comparison results with other state-of-the-art deadlock prevention policies validate its overall advantages in terms of computational complexity, structural complexity, and behavior permissiveness.