Statistical Model Checking of Python Agent-Based Models: An Integration of MultiVeStA and Mesa

Agent-based models (ABM) consist of several heterogeneous agents interacting in a complex way, possibly mediated by spatial constraints or other aspects, giving rise to emergent behavior not directly expressed in the model itself. These aspects made ABMs widespread in several areas, including the social sciences. These models are typically too complex to be solved analytically, requiring to use simulation-based analyses. Often, especially in the social sciences, these simulation-based analyses are not automatic, and the number of performed simulations or simulation steps might be arbitrary. This might lead to replicability issues, to low statistical accuracy of the results, or just to wrong results. In computer science, simulation-based analyses can be automated, e.g., using statistical model checking. We present an integration of the statistical model checker MultiVeStA with Mesa, a python-based framework for modeling and analysing ABMs. We validate the integration by using two seminal ABMs from the social sciences. We analyze the famous Boids flock model, able to generate flocking behaviors of birds, with the transient and counterfactual analysis capabilities of MultiVeStA. We analyze the well-known Schelling model, able to generate social segregation behaviors, with the steady-state and ergodicity diagnostics capabilities of MultiVeStA. The contribution of this paper is not methodological. Rather, this is on the one hand a case study paper presenting an application of MultiVeStA. On the other hand, it is a step towards automating and making more reliable the simulation-based analysis of models written in the popular Mesa framework.