Maximally permissive deadlock prevention via an invariant controlled method

Abstract

Recently, researchers have proposed a novel and computationally efficient method to design optimal control places and an iteration approach that computes the reachability graph once to obtain a maximally permissive, if any, liveness-enforcing supervisor of flexible manufacturing systems (FMS). The approach solves the set of integer linear inequalities to compute control places. If, given a Petri net model, no solution exists, the optimal control place does not exist for the Petri net model. We discover that a solution always exists for systems of simple sequential processes with resources (S3PR), but not for the case of FMS modelled by generalised Petri nets (GPN). We propose a theory to prove that there are no good states that will be forbidden by the control policy for S3PR, in which live and dead states cannot have the same weighted sum of tokens in the complimentary set of a siphon. For a system of simple sequential processes with general resource requirements (S3PGR2) modelled by GPN, we find the reason why the integer linear programming (ILP) may not have solutions, which is consistent with the fact that optimal supervisor synthesis for GPN remains unknown. We show that live and dead states may have the same weighted sum of tokens in the complimentary set of a siphon in a GPN. These theoretical results are verified by case studies.