Reliable and explainable analysis of AVS/RS by Statistical Model Checking and Process Mining

Reliable and explainable analysis of AVS/RS by Statistical Model Checking and Process Mining Emanuele Guerrazzia,∗, Andrea Vandina

arXiv:2611.14371v1 [cs.SE] 10 Nov 2026

a L’EMbeDS, Sant’Anna School of Advanced Studies, Pisa, Italy

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. Keywords: Automated warehousing, Storage and retrieval policies, Discrete Event Simulation, Statistical Model Checking, Process Mining

∗ Corresponding author

Email addresses: emanuele.guerrazzi@santannapisa.it (Emanuele Guerrazzi), andrea.vandin@santannapisa.it (Andrea Vandin)

1. Introduction Automated Vehicle Storage and Retrieval System (AVS/RS) is a type of Autonomous Storage and Retrieval Systems (AS/RS) that gained remarkable popularity over the last two decades [1] and remains widely adopted today thanks to its high throughput, scalability, and energy efficiency [2]. The throughput of such systems is higher compared to previous AS/RS, such as Crane-Based Storage and Retrieval Systems, thanks to the parallelization of operations across multiple vehicles that can work simultaneously on different levels [3]. The same holds for scalability, as additional shuttles can be easily added to a working system [4], and for energy efficiency, as shuttles are less energy-intensive than traditional stacker cranes [5, 6]. These characteristics make AVS/RS particularly suitable for a wide range of warehouse applications, from handling small e-commerce items to managing heavier pallets [7, 8]. Indeed, another key advantage of AVS/RS is the breadth of feasible layouts and design variants. Figure 1 illustrates a representative AVS/RS with eight levels per aisle, a triplecapacity buffer near the I/O, one lift per aisle that serves both unit loads and shuttles (allowing shuttles to change levels), and triple-deep channels. For medium-to-long lane depths (e.g., from about three positions onward), shuttles typically collaborate with a compact satellite vehicle that executes in-channel storage and retrieval operations. Figure 1 (b) shows that this is a multi-deep configuration, as it admits Stocking Keeping Units (SKU) of different size (as opposed to single-deep ones). Due to the inherent complexity of these systems, simulation-based approaches are commonly employed to evaluate their performance under different configurations and operational scenarios. For simulation-based studies to be meaningful, it is essential for them to be statistically valid [10]. In this regard, Statistical Model Checking (SMC) provides a reliable verification method to estimate quantitative performance measures through simulation runs of the system [11, 12]. A particularly suitable variant for engineering applications is black-box SMC, which does not require explicit access to the internal structure of the model and can therefore be applied directly to existing simulators without reformulating their logic into a formal language [13]. This is supported by a number of tools, including MultiVeStA [14, 15, 16] 1 , a general-purpose SMC software capable of tool-chaining with external simulators written multiple languages (e.g, MATLAB, Python, C/++, or Java) [14]. MultiVeStA allows to automate the statistical analysis of complex simulation models while enhancing their reproducibility and accuracy, and it reduces 1 https://github.com/andrea-vandin/MultiVeStA/wiki

2

Figure 1: Basic layout of a multi-deep AVS/RS. The figure shows a storage rack arranged in aisles and levels, shuttles traveling horizontally along each level, and lifts providing vertical transfers between levels and I/O stations. Adapted from [9]

potential biases of simulation-based approaches [14, 17]. Considering specifically AVS/RS models, the integration with MultiVeStA enables rigorous simulationdriven performance evaluation of AVS/RS under different configurations, control strategies, and environmental conditions. However, a well-known limitation of traditional SMC is that results are provided only in the form of numerical estimates, without additional insights into the behaviors that generated them [11, 17]. If a performance metric unexpectedly degrades, the modeler cannot easily determine whether this is due to a true system bottleneck or a modeling flaw. To overcome this black-box limitation, recent works have integrated SMC with Process Mining (PM) [17, 18]. PM is a family of techniques from process-oriented data science that analyse the executions (i.e., traces, or logs) of activities generated by information systems with the goal of identifying process patterns, bottlenecks, and other issues in a model [19]. PM is gaining more and more popularity in industry because visualizing the flow of activities can help identifying opportunities for improvement (see, e.g., the recent study by Deloitte on the industrial adoption of PM [20]). The idea behind the integration 3

of SMC and PM is that, by analysing logs generated by simulations, PM can reconstruct a compact behavioral model (a graphical representation of the behavior) that exposes how the system actually operates. This enables automatic detection of unexpected dynamics, unreachable transitions, and performance-critical paths, improving both model interpretability and trust in the results. So far, the integration of PM and SMC has been investigated in specific modeling domains such as software product lines, collective adaptive systems, or threat modeling [17, 21, 22]. To the best of the authors’ knowledge, only a few SMC approaches to analyse warehousing have been proposed [10], while PM-based approaches are more widespread (see, e.g., [23, 24, 25]). However, no approaches combining SMC and PM have been proposed for warehousing. Furthermore, no SMC or PM alone approaches have ever been applied to AVS/RS systems in warehousing. The goal of this work is to fill these gaps by investigating the suitability of combining SMC and PM for the quantitative and behavioral analysis of AVS/RS simulators. In this way, we aim to get statistically sound and interpretable analysis. To demonstrate the validity and practical relevance of our approach, we created a new, open source, AVS/RS simulator consistent with the operational parameters and design configurations reported in the literature [8]. The simulator is publicly available at [26]2 . This is actually an additional notable contribution of our work, as we are not aware of any other available open source AVS/RS simulator. Overall, this study seeks to address the following Research Question: RQ How can the integration of Statistical Model Checking and Process Mining enhance the reliability and interpretability of simulation-based performance evaluation of AVS/RS? To answer this RQ, we exploit SMC to provide statistically valid performance estimates, while PM is used to extract behavioral models from simulation logs. This combination supports both a rigorous evaluation of AVS/RS performance under alternative stocking and picking policies and an interpretation of performance drivers and bottlenecks through the analysis of execution traces. 2. Related Work This section reviews relevant contributions in three main areas: the application of discrete-event simulation (DES) in AVS/RS (Section 2.1), the integration of Sta2 https://doi.org/10.5281/zenodo.18629711

4

Table 1: Summary of relevant studies on AVS/RS DES, SMC, and PM. Ref.

AS/RS analysed

Goal

Method/SW

Data used

SMC

PM

Code avail.

[27]

AVS/RS Single-deep

Throughput optimization

DES (ARENA)

No

No

No

[28]

Manual Multi-level

Synthetic (simulation scenarios) Real (industrial data) Real

No

No

No

No

No

No

No

No

No

No

No

No

Yes

No

No

Yes

No

No

No

Yes

No

No

Yes

No

No

Yes

No

Yes

Yes

Yes

[5] [29] [30] [10] [31]

[32] [33]

[34]

This work

Order-picking produc- DES tivity with class-based storage AVS/RS Multi-deep Energy consumption DES (MATLAB) and recovery SBS/RS Energy consumption DES (ARENA) Synthetic and recovery AVS/RS Movable- Throughput analysis DES (ARENA) Synthetic lifts Multi-level multi- DT model validation DES (AnyLogic) + Real (labodeep AS/RS DoE ratory data) Multi-robot ware- Functional assurance MDD (BIP) + Synthetic house system and orchestration SMC-BIP + real verification (Robotnik platform) Warehouse Manage- Conformance and bot- PM (ProM – Real (ERP ment (SAP WM) tleneck analysis Heuristic Miner) logs) Internal logistics Value stream mapping PM + value stream Real (interand performance anal- mapping nal logistics ysis event logs) Logistics warehouse End-to-end process PM (ProM – Real (WMS process discovery, confor- Inductive/Heurisevent logs) mance and perfor- tic/Alpha Miner, mance analysis Petri nets) Multi-deep AVS/RS

Throughput and capacity evaluation

DES (MATLAB) + MultiVeStA

Synthetic

tistical Model Checking (SMC) in warehouse systems (Section 2.2), and the application of Process Mining (PM) techniques to warehousing (Section 2.3). These are summarized in Table 1, highlighting how the present study extends the state of the art. The analysis highlights both the advances and the gaps that motivate the integrated framework proposed in this study. 2.1. Discrete-Event Simulation in AVS/RS DES has long been a cornerstone for the design and performance evaluation of AVS/RS as it allows for the detailed representation of their complex interactions and dynamic behavior [35]. It enables engineers to test various control strategies and layout configurations under realistic operating conditions without disrupting real operations [36] or even at the design stage [1], allowing to evaluate “what-if” scenarios. 5

A recent review [37] provides a comprehensive overview of AVS/RS studies based on DES, categorizing them by design and performance objectives. This bibliometric analysis showed that DES remains the dominant method for capturing the stochastic and dynamic nature of AVS/RS operations. The review also identifies significant research gaps concerning stocking and picking policies, highlighting the need for more integrative DES frameworks that encompass physical layout and operational control. In the following, we revisit the studies that most closely resemble the system proposed in this work and the adopted methodological framework. One of the earliest is proposed by Ekren [27], that analysed several configurations of AVS/RS to check their impact on throughput with the commercial software ARENA[38]. In the context of manual multi-level rack distribution warehouses, Chan and Chan [28] use discrete-event simulation to assess how class-based storage policies affect order-picking productivity, further illustrating the suitability of DES for studying storage and retrieval strategies across different warehouse technologies. Other works used DES to evaluate the energy consumption and recovery within warehousing processes, demonstrating substantial energy savings compared to traditional CBAS/RS [5, 29] More recently, several variants of AVS/RS configuration has been studied, such as the movable lifts one proposed by [30] which shows how separating input and output stations leads to higher throughput and better resource balance under the same number of vehicles. In parallel, related shuttle-based storage and retrieval systems (SBS/RS) have been analysed through DES to investigate control policies, such as the free balancing rules studied by Collectively, these works confirm DES as an effective approach for evaluating performance, energy, and scalability trade-offs in AVS/RS designs. 2.2. Integrating Statistical Model Checking in warehousing While DES provides valuable performance insights, it generally lacks guarantees of formal correctness or probabilistic reliability of the observed results. SMC addresses this limitation with formal verification, enabling quantitative estimation of temporal logic properties with user-defined statistical confidence. This approach is particularly useful in complex domains, such as automated warehouses. Yet, as highlighted by Ferrari et al. [10], rigorous validation of simulation models is a prerequisite for any form of trustworthy statistical or simulation-based analysis. Their work demonstrates how a Design of Experiment (DoE) methodology can be effectively employed to calibrate and validate an AS/RS discrete-event model against real laboratory data, ensuring that the digital replica accurately reflects the stochastic behaviour of the physical system. 6

Beyond traditional validation, formal verification has recently emerged as a complementary strategy to ensure the reliability of warehouse automation systems. In this direction, Baouya et al. [31] introduced the BRAIN-IoT framework, which integrates Model-Driven Design with SMC through the Behavior– Interaction–Priority formalism. The framework enables the formal specification and probabilistic verification of orchestrated robotic fleets, offering functional assurance prior to deployment. In the context of AVS/RS, however, SMC has not yet been integrated with existing DES models used directly by practitioners and reserarches in the area. Black-box SMC frameworks such as MultiVeStA [14] can enable this, allowing for the statistically rigorous evaluation of AVS/RS, performance under different layouts and control policies while maintaining compatibility with legacy simulators. Considering specifically MultiVeStA, it has shown its great generality and effectiveness in several domains and simulators such as crowd steering scenarios [39], public transportation systems [40, 41], lending pools in decentralized finance [42], highly-configurable systems [43, 44], business process modeling [45], security threat modeling [46, 47], adaptive robotic systems [48, 49], collective adaptive systems in general [50, 21], agent-based models [14, 51]. 2.3. Process Mining in Warehousing PM techniques allow the extraction, reconstruction, and analysis of event-driven process models from system logs. Initially introduced by [52] and later systematized in [53], PM has become a key tool for bridging the gap between modelbased analysis and real-world system behavior. By uncovering how processes are actually executed, PM enables the detection of deviations, bottlenecks, and inefficiencies that would otherwise remain hidden in traditional modeling approaches. In industrial environments, PM has been increasingly adopted to assess performance and conformance of manufacturing and logistics processes [54, 55]. A notable example in warehousing is provided by [32], who applied process mining to the Warehouse Management module of SAP in a manufacturing company. Using the Heuristic Miner algorithm implemented in ProM[56], they reconstructed the material movement process and compared it with the company’s standard procedure. The analysis revealed additional nonstandard activities, capacity-related bottlenecks, and violations of the FIFO rule, leading to recommendations for warehouse resource balancing and planning stability. In a related context of internal logistics, Knoll et al. [33] integrate multidimensional process mining with value stream mapping to analyze in-plant material flows and identify performance bottlenecks. 7

The more recent contribution of Napieraj [34] extended the application of PM to large-scale logistics operations. They conducted a comprehensive analysis of a real industrial warehouse process using ProM. Their workflow included eventlog preprocessing, process discovery, conformance checking, temporal and organizational mining, and error analysis. By modeling the process as a Petri net and experimenting with multiple discovery algorithms (Inductive Miner, Heuristic Miner, and Alpha Miner), they demonstrated how PM can effectively diagnose deviations, quantify performance, and detect organizational inefficiencies. The study also emphasizes practical aspects such as event-log quality, noise filtering, and concept drift, highlighting PM as a valuable operational tool for continuous improvement in logistics environments. Taken together, the reviewed studies reveal a clear research gap. While DES has been extensively used to evaluate performance and design variants of AVS/RS, few works have pursued statistically rigorous validation, and none have combined such analyses with behavioral interpretation. SMC provides the missing formal layer to quantify uncertainty and ensure result reliability, whereas PM complements it by exposing the underlying operational dynamics hidden in simulation data, but they lack rigorous studies on AVS/RS operations. The convergence of these three perspectives thus offers a promising path toward transparent, reproducible, and interpretable performance evaluation of AVS/RS. 3. Methodology The proposed methodology integrates DES, SMC and PM into a unified framework for the quantitative and behavioral analysis of AVS/RS. The workflow, summarized in Figure 2, consists of three main phases that jointly ensure reproducibility, statistical rigor and interpretability of the simulation results: Modeling the system in a DES tool (Section 3.1); Integrating the model with MultiVeStA (Section 3.2); Process Mining analysis of collected logs (Section 3.3). 3.1. System modeling The system modeling proposed in this work relies upon the development of a DES model due its intrinsic ability to capture the dynamic and complex nature of storage and retrieval tasks carried out inside a highly parallelized system such as AVS/RS [57]. The AVS/RS considered in this study is analogous to the one depicted in Figure 1. We developed a DES model using Matlab, following a modular workflow and according to the well-known methodology of Marchet et al. [1]. In this section we focus only on the software architecture of the model, and on its 8

Figure 2: Proposed methodology integrating DES modeling, SMC, and PM.

main components, while we provide details on the considered scenario in Section 4. Figure 3 summarizes the software architecture of the DES. Initialization and system configuration The first component of the software architecture allows to define the AVS/RS parameters such as geometric configuration (i.e., number and geometric properties of aisles, levels, channels), kinematic data (i.e., velocity, acceleration, and deceleration profiles for lifts, shuttles and satellites), and operational logic (i.e., selection of storage and retrieval policies) through the read_parameters function. Afterwards, the static environment of the warehouse is constructed by using (build_warehouse), initializing the coordinate system of storage cells and populating the rack with an initial inventory snapshot of different Stocking Keeping Units (SKUs) (populate_warehouse). Finally, all shuttles and lifts are created and correctly positioned in their starting position of the warehouse (presimulation). In the output of this module, we have the current state of the warehouse, with the items placed in their initial locations. Workload generation The second module of this DES (generate_orders) is responsible for creating a synthetic workload using appropriate statistical distributions to realistically approximate demand patterns. More specifically, an exponential distribution is used 9

Simulation core

Workload generation

Initialization and system configuration

next event

pop_next_event

generate_orders read_parameters

update_warehouse&server

update_order

build_warehouse order list

stocking

service

order

populate_warehouse

picking

Event Queue presimulation

new_stocking

new_picking

new_service

new event initial inventory

compute_new_event

storage/ retrieval

Warehouse state

event logs

Performance analysis compute_performance

Figure 3: Software architecture of DES

to generate the number of different SKUs, exploiting its intrinsic skewness which mimic demand where a small set of items is ordered very frequently while many items are ordered rarely [58]. The Poisson distribution is the standard model for the count of events occurring in a fixed interval of time or space under the assumptions of independence and a constant average rate, making it a natural choice for modeling arrival counts such as customer orders per day [59]. Finally, to reproduce intraday congestion effects due to demand peak, the normal distribution is used to simulate a peak of activity around 12:30 PM with a spread of ±2 hours, truncated to stay within shift hours (07:00-20:00). This generates a pronounced activity peak around lunchtime and fewer orders in the early morning and late afternoon, yielding a more realistic scenario [60]. Customer orders are generated as collections of SKUs. To capture the granular dynamics of the system, the simulation deconstructs these orders into atomic SKU-level missions. This allows the model to handle the retrieval of multiple items within a single order asynchronously, mirroring real-world parallel processing capabilities. The generated order list is then used to populate the initial state of the event queue. Simulation core The third component is the essence of the whole DES and relies on the wellknown mechanism called Next Event Time Advances, which determines the time 10

of occurrence of futuristic events based on a list [36]. In this way, the simulation clock is updated only when the next event occurs. The mechanism resolves the dynamic evolution of the system through a global event list, which sorts pending events chronologically in order to accomplish the total amount of orders. The main simulation loop functions as follows: • Event Fetching: the earliest scheduled event is extracted from the future event list using the pop_next_event procedure. • Clock Advancement: The simulation clock is advanced to the timestamp associated with the extracted event. • State Update: The system state is updated to reflect the effects of the event (e.g., a shuttle reaching a storage bay or a lift completing a vertical movement). This update is handled by the update_warehouse_and_server function, which is responsible for maintaining the warehouse state as well as the positions and availability of shuttles and lifts. • Order state progression: The corresponding order is updated through the update_order function, which advances the order workflow by one processing step (e.g., a stocking order transitioning from “Shuttle arrival” to “Cell arrival”). • Next event computation: Based on the order type, the subsequent event is determined. This event may correspond to a stocking operation, a picking operation, or a service operation. Service events represent internal system movements, such as a lift repositioning a shuttle across different storage levels without directly serving a picking or stocking request. This subcomponent includes the availability evaluation of constrained resources (i.e., shuttles and lifts). This approach mirrors realistic warehouse operations, where batch processing of orders can improve throughput and reduce shuttle travel distances [61]. During the simulation, all movements, including horizontal shuttle travel, vertical lift operations, and loading/unloading of SKUs, are executed according to the defined kinematic constraints and operational logics. Performance assessment Upon completion of the simulation run, a post-processing routine aggregates the collected data to provide a comprehensive assessment of the AVS/RS system 11

under the given operational parameters. In particular, order-level cycle times are computed separately for the stocking and picking processes, based on the timestamps associated with the main operational activities. In addition, the tunnel occupancy is evaluated, which reflects the capacity of the warehouse and to provide insight into the saturation level of the storage system and its evolution over time under the adopted control policies. Descriptive statistics, specifically the number of instances, and the mean and standard deviation of all the mentioned metrics are calculated to assess the system’s responsiveness, efficiency and variability under a specific workload. Finally, a granular event log is exported: this dataset records every state transition within the system, enabling further offline analyses such as throughput estimation, resource utilization (e.g., shuttle idle/busy time), and bottleneck identification without requiring simulation re-runs. Although this work focuses on cycle-time and occupancy-based performance measures, the proposed framework naturally supports the collection of additional indicators (e.g., resource-level utilization or workload balance), which may be integrated in future analyses without modifying the simulation core. 3.2. Integrating DES with MultiVeStA To enable automated SMC and ensure statistically reliable results, we integrated the DES model of AVS/RS, developed in Matlab, with MultiVeStA, which is a tool-agnostic framework capable of estimating quantitative properties of a system by driving multiple independent simulation runs. The integration follows a black-box approach where MultiVeStA acts as an external coordinator, while the simulator functions as a stepped execution engine. As illustrated in Figure 4, which shows the tool-chaining between MultiVeStA and the DES, this interaction is mediated by a generic Java-based adapter interface. This wrapper abstracts the internal complexity of the Matlab model, exposing only the three fundamental primitives required by the statistical engine: • Reset: Initializes a new simulation run. This method handles the seeding of the random number generator to ensure reproducibility and reloads the preconfigured workspace parameters. • Next Step: Advances the simulation state by one discrete step (invoking the logic described in the previous section). • Evaluate Observation: Queries the current state of the system to extract specific metrics (e.g., current aisle occupancy, task completion time).

12

Figure 4: MultiVeStA tool-chaining with DES

In this workflow, MultiVeStA orchestrates the analysis by repeatedly triggering the simulation steps shown in Figure 3, and by performing online SMC over user-defined properties expressed in a specific language named MultiQuaTEx. The analysis is parametric with respect to the simulation step at which observations are collected, allowing the evaluation of multiple performance indicators, i.e., namely picking cycle time, stocking cycle time, and warehouse utilization at specific stages of the system evolution. For each parameter configuration, MultiVeStA estimates the expected value of the selected observables, enabling a statistically sound comparison of system behavior across different simulation horizons. Batch processing of replications is supported, with parameters controlling the number of independent runs, batch size, and confidence intervals for the statistical estimates. This setup enables comprehensive evaluation of system performance under varying operational conditions, while ensuring reproducibility and modularity of the simulation workflow. 3.3. Process Mining analysis PM is employed in the final phase of the workflow to complement the statistical results produced by MultiVeStA with a behavioral interpretation of the simulated system. While SMC provides quantitative estimates of performance indicators, it does not explain why certain trends emerge or which operational patterns drive the observed results. Recently, an integration of SMC and PM has been proposed to solve this issue [17]. 13

In this paper, we use PM to fill this gap by reconstructing the execution logic of the AVS/RS from the logs generated during simulation, enabling the discovery of process models and the identification of bottlenecks or suboptimal behaviors. The simulation trace is recorded in a tabular format where each row represents a discrete event in the AVS/RS system. The columns are defined as follows: • Order_ID: Unique identifier for the order being processed • SKU_ID: Identifier of the SKU. • Operation type: 0 for Stocking, 1 for Picking, 2 for intermediate lift movements. • Location (Aisle, Level, Channel, Cell): Coordinates determining the storage or retrieval location within the rack system. • Strategy: The storage/retrieval strategy applied (0: Random, 1: Deepest, 2: Nearest). Each strategy is explained in Section 4. • Shuttle_ID: Unique identifier of the shuttle vehicle assigned to the task. • Activity: Description of the specific event occurring (e.g., arrival at I/O, shuttle reservation). • Timestamp: The simulation time (YYYY-MM-DD HH:MM:SS) at which the event occurred. . An extract of the event log is provided by Table 2. Table 2: Fragment of the AVS/RS simulation event log for a stocking operation. Order_ID YYBEJB YYBEJB YYBEJB YYBEJB YYBEJB YYBEJB

SKU_ID AXX AXX AXX AXX AXX AXX

Type 0 0 0 0 0 0

Aisle 5 5 5 5 5

Level 1 1 1 1 1

Ch. 22 22 22 22 22

Cell 1 1 1 1 1

Strat. 0 0 0 0 0

S_ID 5 5 5 5 5

Activity Stocking arrival at I/O Shuttle reservation Lift reservation Lift arrival Shuttle arrival Cell arrival

Timestamp 2025-06-15 09:10:00 2025-06-15 09:10:05 2025-06-15 09:10:07 2025-06-15 09:10:35 2025-06-15 09:11:15 2025-06-15 09:12:00

After the completion of SMC analyses, the obtained logs can be imported into process mining tools such as Disco [62]. Disco automatically generates process maps, a graphical representation of the control-flow extracted from event logs. In a process map, nodes represent activities (e.g., “Shuttle reservation”), while edges 14

Figure 5: Overview of the studied AVS/RS. Panel (a) shows the shuttle operating within a channel, while panel (b) illustrates the lift executing vertical movements between levels. Adapted from [64]

(arrows) represent the directly-follows relationships between activities, indicating which activity typically follows another [53]. Each node and edge is annotated with frequency and performance metrics: for example, an edge may show how many times a particular transition occurred, or the average time elapsed between two activities. This visual representation provides an intuitive overview of the process, making it easier to identify bottlenecks, measure resource utilization, and detect deviations from expected behavior (e.g., violations of stocking or picking policies, which could be use also to validate the simulation model). Specifically, in Section 5.3 we use process maps generated by Disco from the logs of an AVS/RS case study in all of the three picking and stocking strategies to: quantify how often the process follows long execution traces in the three strategy variants; and assess fairness in the utilization of shuttles across the system. 4. Case Study As mentioned, one of the contributions of this paper is a new open-source ASV/RS simulation model, designed following guidelines from the literature, including those concerning warehouse layout structure, vehicle kinematics, and operational assumptions [63, 8]. The considered AVS/RS is based on shuttle technology. Figure 5 shows the two main operating components: (a) the shuttle travelling within a channel, and (b) the lift responsible for vertical movements between levels. The warehouse architecture consists of multiple aisles, each divided into a configurable number of levels, with storage locations arranged along channels within 15

each aisle. The system can accommodate a variable number of shuttles operating along both the aisles and channels, providing scalable storage capacity. The shuttle vehicles are capable of moving horizontally along channels and vertically between levels via lifts to transport goods. Their movement is characterized by controlled acceleration and deceleration, and can be modulated depending on whether the shuttle is carrying a load. Lifts enable vertical movement across tiers, with dedicated inbound and outbound zones for goods handling. The storage/retrieval strategy determines how storage locations are selected for incoming items and how retrieval requests are prioritized within an automated warehouse system. In this case study, three strategies are considered for stocking and picking operations: • Random Storage and retrieval locations are selected randomly among all feasible positions. This strategy is simple to implement and provides a baseline for comparison, but it generally leads to suboptimal travel times and inefficient system utilization [65]. • Deepest Items are stored in or retrieved from the deepest available location along the storage lane. This strategy aims to increase storage density and reduce fragmentation, but may increase travel times for handling equipment [66, 67]. • Nearest The system selects the closest available location to the input/output point or the handling device’s current position. This strategy minimizes travel distance and response time, often resulting in improved throughput and reduced energy consumption [68]. Fixed handling times are considered for loading and unloading operations, ensuring realistic simulation of operational performance [10, 8]. Overall, the system design supports scalability and configurability, allowing adjustment of key parameters such as number of aisles, levels, channels, and shuttles to meet different operational requirements. The simulation relies on a structured set of parameters describing the warehouse geometry, vehicle kinematics, and operational conditions. All values are summarized in Table 3. 16

Category / Parameter

Value

𝑁𝑎 𝑁𝑙 𝑁𝑐 𝑁𝑑 𝑊 𝐷 𝐻

6 6 30 6 0.7 m 1.5 m 1.0 m

Description

Warehouse Structure Number of aisles Number of levels per aisle Number of channels per aisle Maximum slots per tunnel Tunnel width Tunnel depth Level height Vehicle Kinematics 𝑁𝑠 𝑉𝑦1 / 𝑉𝑦0 𝐴 𝑦1 / 𝐴 𝑦0 𝑉𝑥1 / 𝑉𝑥0 𝐴𝑥1 / 𝐴𝑥0 𝑉𝑧1 / 𝑉𝑧0 𝐴𝑧1 / 𝐴𝑧0 𝑡load

10 3 / 3 m/s 2 / 2 m/s2 1.5 / 1.5 m/s 1 / 1 m/s2 1 / 1 m/s 0.5 / 0.5 m/s2 1.5 s

Number of shuttles Shuttle speed (loaded/empty, aisle direction) Shuttle acceleration (aisle direction) Satellite speed (loaded/empty, channel direction) Satellite acceleration (channel direction) Lift speed (loaded/empty, vertical) Lift acceleration (vertical) Loading/unloading time

Orders and Operation 𝑀 SKU distribution Working hours Daily orders 𝜇hours 𝜎hours

20 Skewed random 07:00–20:00 500 (Sat. 30%) 12.5 2

Number of SKU variants One dominant product type Daily operating window Average number of orders Mean order time (peak at 12:30) Std. deviation of order timing

Total slots 𝛼 𝛽 𝛾 Occupied slots Stocking strategies Picking strategies

6480 0.6 0.7 1.0 3,888 0/1/2 0/1/2

Occupancy and policies 𝑁𝑎 · 𝑁𝑙 · 𝑁𝑐 · 𝑁 𝑑 Overall warehouse filling Max tunnel occupancy per aisle-level Max slot occupancy within a tunnel 𝛼 · 6, 480 Random / deepest-first / nearest-available Random / deepest-first / nearest-available

Table 3: Summary of parameters used in the AS/RS simulation.

5. Results and Discussion In this section, we present the quantitative results obtained from the statistical analysis of the outputs produced by the combined use of MultiVeStA and DES (Section 5.1), and application of PM to the event logs generated by DES (Section 5.3). 5.1. MultiVeStA Results To evaluate the impact of different storage and retrieval strategies on system performance, we first estimated key performance indicators for three system configurations (i.e., Random, Deepest, and Nearest policies) under identical operational conditions. Then, we pairwise compared the results obtained using statisti17

Listing 1: MultiQuaTEx parametric query used for the analysis

1 obsAtStep (x,obs) = 2 if ( s.rval("steps ") == x ) 3 then s.rval(obs) 4 else # obsAtStep (x,obs) 5 fi ; 6 7 eval parametric ( 8 E[ obsAtStep (x, " mean_picking_time ") ], 9 E[ obsAtStep (x, " mean_stocking_time ") ], 10 E[ obsAtStep (x, " tunnel_occupancy ") ], 11 x, 1, 1, 72 12 );

cal t-tests to check whether the different settings led to different estimations. This is known as counterfactual analysis [14]. Experimental setup and query definition The analysis was specified using the MultiQuaTEx query language. We defined a parametric query shown in Listing 1. Such query allows to estimate the expected values of three key performance indicators (picking time, stocking time, and tunnel occupancy) at hourly intervals over a simulation horizon of 72 hours. In lines 7-12 we ask MultiVeStA to estimate the expected value of the three key performance indicators at each step x, varying from 1 to 72 hours, with increment 1. For each simulation, we will obtain a real value per combination of step and KPI of interest. In particular, obsAtStep is a so-called recursive temporal operator defined in lines 1-5: for each step of interest x, and each KPI obs, we check whether the simulator (s) has currently performed exactly x steps (line 2). If it is the case, for this simulation, we return the current value of the KPI (line 3). Otherwise, with the # keyword, we ask MultiVeStA to re-evaluate the current x,obs case in the next simulation step. MultiVeStA has two alternative stopping criteria to decide the required number of simulations. One, is given by a maximum admitted confidence interval (CI) specified by the user. This is given in terms of 𝛼 and 𝛿: roughly speaking, we perform enough simulations such that around each estimation given by MultiVeStA we build an interval with statistical confidence (100 − 𝛼)%, and width at most 𝛿. In this way, for each time step 𝑥, MultiVeStA automatically orchestrated the 18

necessary number of independent simulation replications to estimate the expected values with a (100 − 𝛼)% CI. The second stopping criterion, is simply a maximum number of simulations 𝑁. In the latter case, we equip anyway each estimation with the CI obtained with the given simulations (𝛼 shall be specified anyway). In this experiment, we follow the first approach, setting 𝛼 = 10% and 𝛿 = 5 for all the three KPIs. Performance overview Figures 6a, 6b and 6c presents the mean trajectories of the KPIs. The solid lines represent the mean values of the performance indicators, while the shaded bands indicate the corresponding CI, providing a quantitative measure of the statistical reliability of the results. With the selected values for 𝛼 and 𝛿, statistically reliable estimates were achieved with 𝑁 = 20. Specifically, for all the three KPIs the confidence bands satisfy the requirements for a 90 % CI, confirming the adequacy of the chosen number of simulation runs. This is due to the relatively low variance of the process after the initial transient phase, offering an optimal trade-off between statistical robustness and computational cost. The results highlight distinct trade-offs between the strategies: • Random: Achieves stable but suboptimal cycle times. While simple to implement, it leads to inefficient space utilization, as indicated by the higher tunnel occupancy saturation. It is used as baseline for comparison with the other two policies. • Deepest: Shows comparable picking and stocking cycle times to the Random policy but significantly improves warehouse space utilization, measured by tunnel occupancy. This suggests it is a balanced strategy for sustainable long-term operations where space is a constraint. • Nearest: Prioritizes speed, resulting in an improvement respectively of over 25% in picking cycle time and over 30% in stocking cycle time compared to the other strategies. However, this comes at the expense of inefficient warehouse utilization, as the system tends to saturate the most accessible cells quickly, leaving deeper locations unused. 5.2. Counterfactual Statistical Analysis After estimating the mean trajectories, we conducted a counterfactual analysis to assess whether the observed differences between strategies are statisti19

36

Time (seconds)

34 32

Deepest Random Nearest

30 28 26 24 0

8

16

24

32

40

Time step (h)

48

56

64

72

Time (seconds)

(a) Mean picking time

32 30 28 26 24 22 20 18 16 0

Deepest Random Nearest

8

16

24

32

40

Time step (h)

48

56

64

72

48

56

64

72

(b) Mean stocking time

Occupancy (%)

50 45

Deepest Random Nearest

40 35 30 25 200

8

16

24

32

40

Time step (h)

(c) Mean tunnel occupancy

Figure 6: Comparison of mean KPIs obtained with MultiVeStA analysis under different policies

20

cally relevant and detectable. We performed point-wise Welch two-sample 𝑡-tests (𝛼 = 0.025) coupled with a the statistical power assessment relevance assessment. The analysis reveals clear dichotomy between statistical relevance and detectability, as detailed below. Picking Time Analysis For the Deepest policy (Figs. 7a, 7c), the slight increase in picking time starts to be statistically significant after the steady-state phase, while the magnitude of the difference seems not to be much relevant (Fig. 6a). This indicates that the time penalty for digging deep is negligible in practice. Conversely, the Nearest policy (Figs. 7b, 7d) yields strong statistical improvements across the entire horizon, confirming its speed advantage (about 9 seconds) with high statistical power. Stocking Time Analysis A similar pattern is observed for stocking operations. The Deepest policy (Figs. 8a, 8c) shows a statistically significant but practically negligible increase in stocking time, with a mean difference ≈ 1s (Fig. 6b). In contrast, the Nearest policy (Figs. 8b, 8d) consistently delivers strong statistical and practically relevant time savings (about 10 seconds), validating its throughput-oriented design. Tunnel Occupancy Analysis The trade-off is reversed for space utilization. The Deepest policy (Figs. 9a, 9c) achieves a massive, practically relevant reduction in tunnel occupancy (mean difference > 25 percentage points), confirming its superior density (Fig. 6c). The Nearest policy shows statistically valid differences with the baseline (Figs. 9b, 9d) but saturates the tunnel quickly, showing no practical benefit in space management compared to the baseline. The counterfactual analysis confirms both the robustness of the observed effects and the appropriateness of the parameters used in MultiVeStA, as the increasing statistical power over time demonstrates stable system behavior beyond the initial transient phase. 5.3. Process Mining Results While the MultiVeStA analysis demonstrated that distinct stocking and picking policies yield results that are numerically and statistically different, it offers limited insight into the operational patterns driving these variations. To bridge this gap, we employ PM techniques to provide a qualitative and behavioral interpretation of the simulation data. By analyzing the event logs, we can deconstruct the internal 21

(a) t-test results (Random vs. Deepest)

(b) t-test results (Random vs. Nearest)

(c) Statistical power analysis (Random vs. Deepest)

(d) Statistical power analysis (Random vs. Nearest)

Figure 7: Statistical comparison of mean picking time for the Random, Deepest and Nearest policies.

22

(a) t-test results (Random vs. Deepest)

(b) t-test results (Random vs. Nearest)

(c) Statistical power analysis (Random vs. Deepest)

(d) Statistical power analysis (Random vs. Nearest)

Figure 8: Statistical comparison of mean stocking time for the Random, Deepest and Nearest policies.

23

(a) t-test results (Random vs. Deepest)

(b) t-test results (Random vs. Nearest)

(c) Statistical power analysis (Random vs. Deepest)

(d) Statistical power analysis (Random vs. Nearest)

Figure 9: Statistical comparison of mean tunnel occupancy for the Random, Deepest and Nearest policies.

24

workflow of each strategy and identify how specific resource constraints influence the global performance. The impact of different policies on the systems’ dynamics PM analysis revealed significant differences in elevator usage depending on the chosen stocking and picking policy. For the random strategy, the elevator was required in over 80% of operations. In contrast, the deepest policy necessitated elevator movements in only about 60% of cases. Interestingly, the nearest strategy exhibited the opposite behavior, with the elevator being avoided in over 92% of operations, resulting in more efficient cycle times. Figure 10 visualizes the process maps obtained from the simulation logs for the three strategies. These maps highlight the frequency and sequence of activities, clearly illustrating how different policies impact the flow of goods and the utilization of vertical transport resources. Performance study The process mining analysis illustrated in Figure 11 shows the mean duration time per activity, highlighting those that contribute most significantly to the overall cycle time. Across all simulated scenarios, picking operations emerge as the most timeconsuming. Specifically, the stages from the initiation of the picking shuttle request to the moment the SKU is loaded onto the shuttle, as well as from the shuttle release by the elevator to the SKU being fully onboard, dominate the process duration. The second most time-intensive activity corresponds to the completion of stocking operations, measured from the arrival of the stocking shuttle to the final placement of the SKU in its designated cell. These insights provide a clear indication of process bottlenecks and critical activities that have the greatest impact on warehouse throughput. Fairness of resource utilization An additional analysis was conducted to evaluate the fairness of resource utilization across different stocking and picking policies. Fairness was quantified using the Jain’s Fairness Index, defined as: ( ∑𝑛

)2 𝑥 𝑖 𝐽 (𝑥 1 , 𝑥 2 , . . . , 𝑥 𝑛 ) = ∑𝑖=1 𝑛 𝑛 𝑖=1 𝑥𝑖2 where 𝑥𝑖 represents the number of tasks assigned to shuttle 𝑖, and 𝑛 is the total number of shuttles. A value close to 1 indicates a perfectly fair distribution of 25

26 (b) Deepest policy

(c) Nearest policy

Figure 10: Process maps for the different stocking and picking policies. The structural differences among the policies highlight their impact on system dynamics and lift utilization.

(a) Random policy

27 (b) Deepest strategy

(c) Nearest strategy

Figure 11: Process mining performance analysis. Each edge reports the mean duration time per activity.

(a) Random strategy

tasks, whereas lower values indicate that some shuttles are more heavily loaded than others. The results, presented in Figure 12, show that the random policy achieves the highest fairness (Jain index = 0.719), distributing tasks more evenly among shuttles. Conversely, the nearest policy, while achieving higher throughput, results in an uneven workload, penalizing some shuttles (Jain index = 0.287). The deepest policy exhibits intermediate behavior, balancing efficiency and fairness (Jain index = 0.673). 6. Discussion 6.1. Theoretical Contribution The theoretical contribution of this research addresses the formulated RQ as follows: (RQ) How can the integration of Statistical Model Checking and Process Mining enhance the reliability and interpretability of DES-based performance evaluation in AVS/RS? This study represents the first attempt to combine such techniques to effectively evaluate AVS/RS performance, showing that the integration of SMC and PM enables a deeper and more interpretable evaluation of stocking and picking policies in AVS/RS compared to relying on simulation-based performance metrics alone. Indeed, while SMC provides statistically sound estimates of how the three analyzed policies affect KPIs such as cycle time and warehouse utilization, PM expands the insights by moving the scope from a broader view to a closer one, i.e., inspecting the impact on each activity of the process. The discovered process maps reveal how different stocking and picking strategies shape system dynamics, particularly in terms of resource interaction and congestion. For instance, policies that appear efficient according to average cycle time can be shown, through PM, to induce specific bottlenecks such as repeated elevator loops or showing unbalanced shuttle utilization. These behavioral patterns are not directly observable from aggregate SMC results, yet they play a crucial role in explaining performance variability. To ensure reproducibility and facilitate further research in this domain, we complement our methodological contribution with the release of an open-source, parameterizable AVS/RS simulator designed according to contemporary industrial guidelines and operational parameters documented in the literature [8]. To the best of our knowledge, this represents the first publicly available discrete-event simulator specifically developed for multi-deep AVS/RS configurations with configurable layout characteristics, control policies, and operational parameters. 28

Number of Tasks

3500 3000 2500 2000 1500 1000 500 0

2

4

6

Shuttle ID

8

10

8

10

Number of Tasks

(a) Random policy

4000 3500 3000 2500 2000 1500 1000 500 0

2

4

6

Shuttle ID

(b) Deepest policy

Number of Tasks

10000 8000 6000 4000 2000 0

2

4

Shuttle ID

6

8

(c) Nearest policy

Figure 12: Shuttle task distribution under different stocking and picking policies

29

6.2. Managerial Implication From a managerial perspective, the proposed integrated framework provides decision-makers with actionable insights that go beyond traditional performance rankings. The comparative analysis of the three policies (random, deepest, and nearest) supported by SMC enables managers to reliably quantify the trade-offs between competing objectives, namely cycle times and efficient warehouse occupancy. Beyond performance rankings, the addition of PM analysis allows the identification of operational mechanisms responsible for these outcomes, for instance, how lift congestion emerges under deepest allocation or how shuttle travel distances vary with nearest placement. This dual perspective supports informed policy selection by clarifying not only which strategy performs better on average, but also how and where inefficiencies emerge within the operational workflow. In practical terms, warehouse managers can exploit this approach to diagnose critical process segments, such as lift usage or shuttle allocation, that are most sensitive to policy choices. This allows targeted interventions, for example redesigning resource coordination rules or introducing control strategies to mitigate congestion, rather than relying on global policy changes. Moreover, the interpretability provided by process models enhances trust in simulation results, facilitating communication between technical analysts and managerial stakeholders. Finally, the integration of SMC and PM supports risk-aware decision-making. By coupling statistically validated performance estimates with behavioral explanations of rare but critical system states, managers are better equipped to evaluate trade-offs between efficiency, robustness, and operational stability. 7. Conclusions & Future Works This work demonstrates the value of combining DES, MultiVeStA, and Process Mining for the analysis of AVS/RS systems. The case study highlights that the selection of picking and stocking policies critically influences both cycle times and warehouse space utilization. Among the tested strategies, the deepest-first policy offers the most balanced trade-off between operational performance and storage efficiency, whereas the nearest-available policy reduces cycle times at the cost of less efficient use of space. The random policy emerges as the least effective overall. The integration of SMC and PM proved particularly valuable: statistical estimates grounded in MultiVeStA can be directly related to the behavioral structures extracted from event logs, revealing the operational mechanisms that drive performance outcomes. This dual quantitative–behavioral perspective enhances inter-

30

pretability, transparency, and trust in simulation results, especially in systems as complex and configuration-rich as AVS/RS. The proposed methodology equips warehouse managers and system designers with actionable insights, enabling informed decisions on operational and tactical strategies. In practice, policies could be alternated dynamically according to business needs, balancing efficiency and space usage over time. Moreover, the framework is general and can be easily transferred to other automated warehousing systems and logistics environments based on DES. Beyond the results presented here, this work provides a foundation for reliable and explainable analysis of AVS/RS and sets the stage for future developments at the intersection of simulation, formal verification, and data-driven process analysis, thus opening several promising research directions Future work will focus on refining this mapping, exploring richer behavioral abstractions, and quantifying the influence of specific process deviations on performance estimates. In addition, an important next step is to replicate the analysis using a real AVS/RS model or real-time operational data. This would allow validating the approach under realistic conditions, assessing its robustness in dynamic environments, and supporting the development of digital twin–based decision-making. A limitation of this study is the evaluation window, which spans only a limited simulation horizon. To properly assess the reliability of the proposed framework under realistic operational scenarios, future work should extend the analysis over extended periods (e.g., 3–4 months of simulated operation) to capture seasonal demand fluctuations, supply chain disruptions, and long-term performance degradation. Such extended analyses would enable a more robust understanding of policy robustness across varying market conditions and inventory dynamics. Further research will also explore hybrid and adaptive policies, sensitivity analyses under varying demand profiles, and tighter integration with online monitoring systems to enable truly data-driven and responsive warehouse operations. References [1] G. Marchet, M. Melacini, S. Perotti, E. Tappia, Development of a framework for the design of autonomous vehicle storage and retrieval systems, International Journal of Production Research 51 (2013) 4365–4387. doi: 10.1080/00207543.2013.778430. [2] Y. Yu, J. Yang, X. Guo, Retrieval sequencing in autonomous vehicle storage and retrieval systems, International Journal of Production Research 31

61 (2023) 8634–8653, export Date: 28 October 2025; Cited By: 12. doi:10.1080/00207543.2022.2158244. URL https://www.scopus.com/inward/record.uri?eid=2-s2. 0-85146746373&doi=10.1080%2f00207543.2022.2158244& partnerID=40&md5=09403f669f23080ac4b6f1b7f4aeddcd [3] T. Lerher, M. Ficko, I. Palčič, Throughput performance analysis of automated vehicle storage and retrieval systems with multiple-tier shuttle vehicles, Applied Mathematical Modelling 91 (2021) 1004–1022. doi:10. 1016/j.apm.2020.10.032. [4] B. Y. Ekren, T. Lerher, M. Küçükyaşar, B. Jerman, Cost and performance comparison of tier-captive sbs/rs with a novel avs/rs/ml, International Journal of Production Research 62 (2024) 1648–1662. doi:10.1080/00207543. 2023.2199101. [5] E. Guerrazzi, V. Mininno, D. Aloini, R. Dulmin, C. Scarpelli, M. Sabatini, Energy evaluation of deep-lane autonomous vehicle storage and retrieval system, Sustainability (Switzerland) 11 (2019). doi:10.3390/su11143817. [6] B. Y. Ekren, A multi-objective optimisation study for the design of an avs/rs warehouse, International Journal of Production Research 59 (2021) 1107–1126, export Date: 28 October 2025; Cited By: 60. doi:10.1080/00207543.2020.1720927. https://www.scopus.com/inward/record.uri?eid=2-s2. URL 0-85078928052&doi=10.1080%2f00207543.2020.1720927& partnerID=40&md5=e3c256925adaee7894374dcd927a9fa7 [7] N. Boysen, R. de Koster, F. Weidinger, Warehousing in the e-commerce era: A survey (9 2019). doi:10.1016/j.ejor.2018.08.023. [8] G. Lupi, R. Accorsi, I. Battarra, R. Manzini, G. Sirri, Space efficiency and throughput performance in avs/rs under variant lane depths, International Journal of Advanced Manufacturing Technology 131 (2024) 1449–1466. doi:10.1007/s00170-024-13160-3. [9] M. KüçükyaÅŸar, B. Y. Ekren, T. Lerher, 13 - energy efficient automated warehouse design, in: J. R. Vacca (Ed.), Solving Urban Infrastructure Problems Using Smart City Technologies, Elsevier, 2021, pp. 269–292. doi:https://doi.org/10.1016/B978-0-12-816816-5.00013-9. 32

URL https://www.sciencedirect.com/science/article/pii/ B9780128168165000139 [10] A. Ferrari, A. Carlin, C. Rafele, G. Zenezini, A method for developing and validating simulation models for automated storage and retrieval system digital twins, International Journal of Advanced Manufacturing Technology 131 (2024) 5369–5382. doi:10.1007/s00170-023-12660-y. [11] G. Agha, K. Palmskog, A survey of statistical model checking, ACM Transactions on Modeling and Computer Simulation 28 (2018) 1–39. doi:10. 1145/3158668. [12] K. Sen, M. Viswanathan, G. Agha, Vesta: A statistical model-checker and analyzer for probabilistic systems, in: Proceedings of the 17th Conference on Computer Aided Verification (CAV’05), Springer, 2005. [13] K. Sen, M. Viswanathan, G. Agha, Statistical model checking of black-box probabilistic systems, in: K. Etessami, S. K. Rajamani (Eds.), 17th International Conference on Computer Aided Verification (CAV 2005), Edinburgh, Scotland, UK, July 6–10, 2005, Proceedings, Vol. 3576 of Lecture Notes in Computer Science, Springer, 2005, pp. 266–280. doi:10.1007/11513988_ 26. URL https://people.eecs.berkeley.edu/~ksen/papers/statver. pdf [14] A. Vandin, D. Giachini, F. Lamperti, F. Chiaromonte, Automated and distributed statistical analysis of economic agent-based models, Journal of Economic Dynamics and Control 143 (10 2022). doi:10.1016/j.jedc.2022. 104458. [15] S. Gilmore, D. Reijsbergen, A. Vandin, Transient and steady-state statistical analysis for discrete event simulators, in: IFM, Springer, 2017, pp. 145–160. [16] S. Sebastio, A. Vandin, MultiVeStA: statistical model checking for discrete event simulators, in: Proc. of ValueTools’13, ICST/ACM, 2013, pp. 310– 315. [17] R. Casaluce, A. Burattin, F. Chiaromonte, A. L. Lafuente, A. Vandin, Whitebox validation of quantitative product lines by statistical model checking and process mining, Journal of Systems and Software 210 (4 2024). doi:10. 1016/j.jss.2024.111983. 33

[18] R. Casaluce, A. Burattin, F. Chiaromonte, A. Vandin, Process mining meets statistical model checking: Towards a novel approach to model validation and enhancement, in: C. Cabanillas, N. F. Garmann-Johnsen, A. Koschmider (Eds.), Business Process Management Workshops - BPM 2022 International Workshops, Münster, Germany, September 11-16, 2022, Revised Selected Papers, Vol. 460 of Lecture Notes in Business Information Processing, Springer, 2022, pp. 243–256. doi:10.1007/978-3-031-25383-6\_18. URL https://doi.org/10.1007/978-3-031-25383-6_18 [19] W. M. van der Aalst, Process Mining, 2nd Edition, Springer, 2016. [20] Deloitte, Deloitte global process mining survey, accessed on 13/01/2026 (2025). URL https://bit.ly/deloittePMIndustry [21] R. Casaluce, M. Tschaikowski, A. Vandin, White-box validation of collective adaptive systems by statistical model checking and process mining, in: T. Margaria, B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola - 12th International Symposium, ISoLA 2024, Crete, Greece, October 27-31, 2024, Proceedings, Part I, Vol. 15219 of Lecture Notes in Computer Science, Springer, 2024, pp. 204–222. doi:10.1007/ 978-3-031-73709-1\_13. URL https://doi.org/10.1007/978-3-031-73709-1_13 [22] R. Casaluce, A. Burratin, F. Chiaromonte, A. Lluch-Lafuente, A. Vandin, Enhancing threat model validation: A white-box approach based on statistical model checking and process mining, in: B. Breve, G. Desolda, V. Deufemia, L. D. Spano (Eds.), Proceedings of the First International Workshop on Detection And Mitigation Of Cyber attacks that exploit human vuLnerabilitiES (DAMOCLES 2024) co-located with 17th International Conference on Advanced Visual Interfaces (AVI 2024), Arenzano (Genoa), Italy, Arenzano, Italy, June 4th, 2024, Vol. 3713 of CEUR Workshop Proceedings, CEURWS.org, 2024, pp. 9–20. URL https://ceur-ws.org/Vol-3713/paper_2.pdf [23] I. Liiv, O. Lepik, Business process mining in warehouses: a case study, in: Proceedings of the 11th International Baltic Conference on Databases and Information Systems, TUT Press, 2014, pp. 387–394. 34

[24] S. Kedem-Yemini, N. S. Mamon, G. Mashiah, An analysis of cargo release services with process mining: A case study in a logistics company, in: Proceedings of the International Conference on Industrial Engineering and Operations Management, Washington DC, USA, 2018, pp. 725–736. [25] S. Montianrat, Analysis of warehouse operations using process mining, 2020. [26] E. Guerrazzi, A. Vandin, AVS/RS Simulator - MultiVeSta Integration (2025). doi:10.5281/zenodo.18629711. URL https://doi.org/10.5281/zenodo.18629711 [27] B. Y. Ekren, S. S. Heragu, Simulation based performance analysis of an autonomous vehicle storage and retrieval system, Simulation Modelling Practice and Theory 19 (2011) 1640–1650. doi:10.1016/j.simpat.2011.02. 008. [28] F. T. S. Chan, H. K. Chan, Improving the productivity of order picking of a manual-pick and multi-level rack distribution warehouse through the implementation of class-based storage, Expert Systems with Applications 38 (3) (2011) 2686–2700. doi:10.1016/j.eswa.2010.08.058. [29] B. Y. Ekren, A simulation-based experimental design for sbs/rs warehouse design by considering energy related performance metrics, Simulation Modelling Practice and Theory 98 (2020) 101991. doi:https://doi.org/10.1016/j.simpat.2019.101991. https://www.sciencedirect.com/science/article/pii/ URL S1569190X19301248 [30] B. Jerman, B. Y. Ekren, M. Küçükyaşar, T. Lerher, Simulation‐based performance analysis for a novel avs/rs technology with movable lifts, Applied Sciences (Switzerland) 11 (2021) 1–16. doi:10.3390/app11052283. [31] A. Baouya, S. Chehida, S. Bensalem, L. Gürgen, R. Nicholson, M. Cantero, M. Diaznava, E. Ferrera, Deploying warehouse robots with confidence: the brain-iot framework’s functional assurance, Journal of Supercomputing 80 (2024) 1206–1237. doi:10.1007/s11227-023-05483-x. [32] E. R. Mahendrawathi, H. M. Astuti, I. R. K. Wardhani, Material movement analysis for warehouse business process improvement with process mining: A case study, in: Lecture Notes in Business Information Processing, Vol. 219, 35

Springer Verlag, 2015, pp. 115–127. doi:10.1007/978-3-319-19509-4_ 9. [33] D. Knoll, G. Reinhart, M. Prüglmeier, Enabling value stream mapping for internal logistics using multidimensional process mining, Expert Systems with Applications 124 (2019) 130–142. doi:10.1016/j.eswa.2019.01.026. [34] A. Napieraj, N. Pyzik, Analysis of a logistics process based on the event log, Applied Sciences (Switzerland) 15 (8 2025). doi:10.3390/app15168968. [35] S. Derhami, J. S. Smith, K. R. Gue, A simulation-based optimization approach to design optimal layouts for block stacking warehouses, International Journal of Production Economics 223 (2020) 107525. doi:https://doi.org/10.1016/j.ijpe.2019.107525. URL https://www.sciencedirect.com/science/article/pii/ S0925527319303524 [36] K. Agalianos, S. T. Ponis, E. Aretoulaki, G. Plakas, O. Efthymiou, Discrete event simulation and digital twins: Review and challenges for logistics, in: Procedia Manufacturing, Vol. 51, Elsevier B.V., 2020, pp. 1636–1641. doi: 10.1016/j.promfg.2020.10.228. [37] E. B. Kızılırmak, S. Öztaş, N. Çağlayan, M. Tutam, Design and performance measures of avs/r systems: A bibliometric literature review (8 2024). doi: 10.1007/s11831-024-10084-9. [38] Rockwell Automation, Arena simulation software, commercial simulation software (2025). URL https://www.rockwellautomation.com/en-us/products/ software/arena-simulation.html [39] D. Pianini, S. Sebastio, A. Vandin, Distributed statistical analysis of complex systems modeled through a chemical metaphor, in: HPCS, 2014, pp. 416– 423. [40] S. Gilmore, M. Tribastone, A. Vandin, An analysis pathway for the quantitative evaluation of public transport systems, in: IFM, 2014. [41] V. Ciancia, D. Latella, M. Massink, R. Paškauskas, A. Vandin, A tool-chain for statistical spatio-temporal model checking of bike sharing systems, in: ISOLA’17, 2017. 36

[42] M. Bartoletti, J. H. Chiang, T. Junttila, A. Lluch-Lafuente, M. Mirelli, A. Vandin, Formal analysis of lending pools in decentralized finance, in: Proc. of ISoLA 2022, Vol. 13703 of LNCS, Springer, 2022, pp. 335–355. [43] M. H. ter Beek, A. Legay, A. Lluch-Lafuente, A. Vandin, A Framework for Quantitative Modeling and Analysis of Highly (Re)configurable Systems, IEEE Trans. Software Eng. 46 (3) (2020) 321–345. [44] A. Vandin, M. H. ter Beek, A. Legay, A. Lluch-Lafuente, QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems, in: FM, 2018. [45] F. Corradini, F. Fornari, A. Polini, B. Re, F. Tiezzi, A. Vandin, A formal approach for the analysis of BPMN collaboration models, JSS 180 (2021) 111007. [46] M. H. ter Beek, A. Legay, A. L. Lafuente, A. Vandin, Quantitative security risk modeling and analysis with RisQFLan, Computers & Security 109 (2021) 102381. [47] R. Casaluce, A. Burattin, F. Chiaromonte, A. Vandin, Process mining meets statistical model checking: Towards a novel approach to model validation and enhancement, in: C. Cabanillas, N. F. Garmann-Johnsen, A. Koschmider (Eds.), BPM Workshops, Springer, 2023, pp. 243–256. [48] L. Belzner, R. D. Nicola, A. Vandin, M. Wirsing, Reasoning (on) service component ensembles in rewriting logic, in: S. Iida, J. Meseguer, K. Ogata (Eds.), Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi, Vol. 8373 of Lecture Notes in Computer Science, Springer, 2014, pp. 188–211. [49] R. Bruni, A. Corradini, F. Gadducci, A. Lluch-Lafuente, A. Vandin, Modelling and analyzing adaptive self-assembly strategies with maude, Sci. Comput. Program. 99 (2015) 75–94. [50] V. Galpin, A. Georgoulas, M. Loreti, A. Vandin, Statistical analysis of CARMA models: an advanced tutorial, in: B. Johansson, S. Jain (Eds.), Proc. of WSC, IEEE, 2018, pp. 395–409. doi:10.1109/WSC.2018.8632456. [51] A. Vandin, Statistical model checking of python agent-based models: An integration of multivesta and mesa, in: Bridging the Gap Between AI and Reality: Second International Conference, AISoLA 2024, Crete, Greece, October 37

30 – November 3, 2024, Proceedings, Springer-Verlag, Berlin, Heidelberg, 2025, p. 398–419. doi:10.1007/978-3-031-75434-0_26. URL https://doi.org/10.1007/978-3-031-75434-0_26 [52] W. M. P. van der Aalst, T. Weijters, L. Maruster, Workflow mining: Discovering process models from event logs, IEEE Transactions on Knowledge and Data Engineering 16 (9) (2004) 1128–1142. doi:10.1109/TKDE.2004.47. [53] W. M. P. van der Aalst, Process Mining: Data Science in Action, 2nd Edition, Springer, Berlin, Germany, 2016. doi:10.1007/978-3-662-49851-4. [54] C. d. S. Garcia, A. Meincheim, E. R. Faria Junior, M. R. Dallagassa, D. M. V. Sato, D. R. Carvalho, E. A. P. Santos, E. E. Scalabrin, Process mining techniques and applications – a systematic mapping study, Expert Systems with Applications 133 (2019) 260–295. doi:10.1016/j.eswa.2019.05.003. [55] J. Alnahas, Application of process mining in logistic processes of manufacturing organizations: A systematic review, Sustainability 15 (15) (2023) 11783. doi:10.3390/su151511783. URL https://doi.org/10.3390/su151511783 [56] ProM Tools, Prom: Process mining framework, open-source framework for process mining (2025). URL https://promtools.org/ [57] S. Derhami, J. S. Smith, K. R. Gue, A simulation-based optimization approach to design optimal layouts for block stacking warehouses, International Journal of Production Economics 223 (2020) 107525. doi:https://doi.org/10.1016/j.ijpe.2019.107525. URL https://www.sciencedirect.com/science/article/pii/ S0925527319303524 [58] M. Merschformann, T. Lamballais, M. de Koster, L. Suhl, Decision rules for robotic mobile fulfillment systems, Operations Research Perspectives 6 (2019) 100128. doi:https://doi.org/10.1016/j.orp.2019.100128. https://www.sciencedirect.com/science/article/pii/ URL S2214716019300946 [59] C. Lorenz, A. Otto, M. Gendreau, Picking operations in warehouses with dynamically arriving orders: How good is reoptimization?, Networks 86 (2) (2025) 157–173. arXiv:https: 38

//onlinelibrary.wiley.com/doi/pdf/10.1002/net.22281, doi:https://doi.org/10.1002/net.22281. URL https://onlinelibrary.wiley.com/doi/abs/10.1002/net. 22281 [60] Y. Liu, H. Zhang, J. Wang, Research on dynamic prediction model of orders in e-commerce distribution center based on ga-bp neural network, in: Proceedings of the 2020 International Conference on Logistics Engineering and Intelligent Transportation Systems, Atlantis Press, 2020, pp. 1–6. doi:10.2991/aebmr.k.201203.001. [61] H. Xu, J. Shao, Y. Sun, Research on order batching optimization based on improved NSGA-II algorithm, PLoS One 20 (2) (2025) e0319182. doi: 10.1371/journal.pone.0319182. [62] Fluxicon, Disco: Process mining software, software project (2025). URL https://fluxicon.com/disco/ [63] I. Battarra, R. Accorsi, R. Manzini, S. Rubini, Hybrid model for the design of a deep-lane multisatellite avs/rs, International Journal of Advanced Manufacturing Technology 121 (2022) 1191–1217. doi:10.1007/ s00170-022-09375-x. [64] E. Guerrazzi, V. Mininno, D. Aloini, Balancing picking and outbound loading efficiency in an sbs/rs through a digital twin, Flexible Services and Manufacturing JournalCited by: 1; All Open Access, Hybrid Gold Open Access (2024). doi:10.1007/s10696-024-09554-w. URL https://www.scopus.com/inward/record.uri?eid=2-s2. 0-85195980418&doi=10.1007%2fs10696-024-09554-w&partnerID= 40&md5=00bee5b2f2e95337d42b0975a1e72197 [65] T. Lehmann, J. Hußmann, Travel time model for multi-deep automated storage and retrieval system with a homogeneous allocation structure, Logistics Research 14 (5), conferma l’uso della Random policy nei modelli di tempo di viaggio per sistemi multi-deep. (2021). doi:10.23773/2021_5. [66] T. Lerher, J. Marolt, F. Sgarbossa, B. Y. Ekren, G. Dukic, Design and Operation of Single- and Multi-deep Shuttle-Based Storage and Retrieval Systems (SBS/RS), Springer International Publishing, Cham, 2024, pp. 333– 375. doi:10.1007/978-3-031-50273-6_13. URL https://doi.org/10.1007/978-3-031-50273-6_13 39

[67] T. Lerher, M. Sraml, I. Potrc, M. Borovinsek, Travel time model for doubledeep automated storage and retrieval systems, International Journal of Production Research 48 (11) (2010) 3151–3172, tratta le implicazioni delle strategie multi-deep (deepest) sui tempi di viaggio. [68] S. E. McInerney, et al., Increasing warehouse throughput through the implementation of class-based storage, South African Journal of Industrial Engineering 33 (2), descrive la politica ”Closest-Open” (Nearest) come quella che assegna il bin vuoto più vicino. (2022).

40

Related documents

• Group-based privacy preservation techniques for process mining#1092023
• Modeling and Verification of Randomized Distributed Real -Time Systems#472214
• Themis: A Filesystem Model Checker That Owns the Machine#424052
• Opacity of Parametric Discrete Event Systems: Models, Decidability, and Algorithms#1458134
• Combining model checking with simulation-based techniques for protocol verification#386960