Abstract In this work, we present an industrial case study of deadlock avoidance in the context of automated warehouse logistics. In particular, we consider systems of Automated Guided Vehicles (AGVs) in which semi-autonomous robots move inside a facility along a predefined set of paths. The paper introduces a novel formalization of AGV systems that models the physical setup of the AGV system more accurately compared to previous approaches. In particular, our modeling approach captures movement restrictions due to physical proximity of vehicles regardless of the logical connectivity of the guide path network. The paper provides and compares three different encodings of such models as transition systems, which enable symbolic analysis of the system via Binary Decision Diagrams (BDDs). Based on these encodings we perform deadlock avoidance for warehouse layouts of both synthetic and real-world origin.