Formal verification of deadlock avoidance rules for AGV systems

Automated Guided Vehicles (AGVs) are increasingly popular and bring many industrial benefits. However, when a number of AGVs autonomously execute their itineraries, it is possible for two or more AGVs to prevent each other from completing their tasks and cause a deadlock from where the system cannot progress. One way that companies try to avoid this is to, based on simulations, generate deadlock avoidance rules (DA-rules) that determine for different scenarios how the AGVs should behave. This paper presents an application of translating such DA-rules to extended finite-state automata and then to formally verify if the rules actually do avoid deadlocks. This is done by using information of an existing system setup where there are two major types of DA-rules. Both of these can be modelled as automata with guards and actions that prevent a transition from occurring if associated conditions are not fulfilled. These guards are generated automatically for all the DA-rules corresponding to the current itineraries. For a chosen itinerary a complete automaton is generated, as well as automata representing the DA-rules. Using the supervisor synthesis tool SUPREMICA, it is shown that the existing DA-rules do not manage to remove all deadlocks in all cases. Even worse, the DA-rules can lead to a fully blocking system, even though a deadlock-free solution does exist, as can be shown by computing a supervisor for the system without the DA-rules