Open Source MATLAB Implementation of AVS/RS with SMC

This repository provides the reference implementation of the AVS/RS with SMC framework presented in the article “Reliable and explainable analysis of AVS/RS by Statistical Model Checking and Process Mining” submitted to the journal "Expert Systems with Applications". The framework integrates: a configurable MATLAB-based discrete-event simulator of Automated Vehicle Storage and Retrieval Systems (AVS/RS), Statistical Model Checking (SMC) through MultiVeStA for statistically reliable performance estimation with user-defined confidence levels, post-simulation statistical and counterfactual analysis tools, structured event log generation for Process Mining (PM) investigations. MultiVeStA orchestrates multiple independent simulation runs in a black-box fashion to produce statistically validated estimates of key performance indicators such as cycle times, throughput, and storage utilization. The generated event logs enable behavioral diagnostics and bottleneck identification via Process Mining techniques, bridging the gap between quantitative performance verification and operational explainability. The simulator is configured according to recent industrial AVS/RS design guidelines and supports alternative stocking and picking policies (random, deepest, nearest). This repository enables full reproducibility of the experimental results reported in the associated article and provides a reusable toolchain for research on automated warehousing systems. The framework has been tested with MATLAB R2024b, Java 11, and Python 3.x