arXiv:2611.14371v1 Announce Type: cross Abstract: Automated Vehicle Storage and Retrieval Systems (AVS/RS) are increasingly adopted to boost warehouse throughput while containing operational costs. We present an integrated analysis framework that couples discrete-event simulation with Statistical Model Checking (SMC) and Process Mining (PM) to quantify and explain AVS/RS performance. SMC, implemented through the MultiVeStA tool, delivers statistically reliable estimates of key indicators, such as cycle times, throughput, and storage utilization, across alternative stocking and picking policies with user-specified confidence levels. MultiVeStA orchestrates multiple independent simulations in a black-box manner, enabling automated verification. PM ingests the resulting event logs to uncover the behavioral patterns and bottlenecks that drive those indicators, closing the interpretability gap typical of simulation studies. We instantiate the framework on a new open-source AVS/RS simulator configured according to recent industrial guidelines and evaluate multiple control strategies. Results show that the joint use of SMC and PM enables both predictive what-if analyses and post-hoc diagnostics, providing the first combined SMC+PM assessment of AVS/RS operations and a reusable toolchain for automated warehousing research.