Some Limitations of Structure-based Methods for Deadlock Detection Problems of S⁴PR

As a subclass of Petri Nets (PNs), Systems of Sequential Systems with Shared Process Resources (S⁴PR) have been widely used in modelling and analyzing automated manufacturing systems (AMS). Multiple tasks competing for limited shared resources may lead to deadlocks, affecting the desired operation of AMS. Popular methods for deadlock detection are based on traversing a PN's reachability trees/graph from initial markings, but their computational complexity increases exponentially with the number of possible states (markings). To avoid state space analysis, researchers propose various methods for characterizing deadlocks of S⁴PR with structural objects. However, the existing structure-based methods may obtain some fictitious deadlocks, i.e., those that AMS never enters. This paper analyzes the performance of structure-based methods for deadlock detection in S⁴PR through case studies. We show that deadlocks obtained with those techniques are not guaranteed reachable from an initial marking. Hence, additional analyses are required.