MARS @ ETAPS 2026 Accepted MultiVeStA ABM

Statistical Model Checking
of an Island Model for Economic Growth

Stefano Blando  ·  Giorgio Fagiolo  ·  Daniele Giachini  ·  Andrea Vandin  ·  Ernest Ivanaj

📄 Paper PDF 🔬 MultiVeStA on GitHub 💻 Replicability Package

The Model

Technology Space & Agent Dynamics

The economy is a T×T grid of islands — each a productive niche with fitness increasing with distance from the centre. 20 agents choose each period whether to mine, imitate, or explore. The tension between safe exploitation and risky exploration generates endogenous growth.

0.000

Island brightness encodes fitness (distance from centre). Agents shown in blue (Miners), green (Imitators), amber (Explorers). Green arcs = skill transfer during imitation. GDP mini-chart tracks aggregate output in real time.

Miner

Stays on current island. Output ∝ island fitness × own skill. Skills accumulate with each step.

Imitator

Moves to the best visible agent's island and attempts skill transfer with probability φ.

Explorer

Searches for new islands. Switches to a random island with probability ε each period.

Symbol Meaning Baseline

Standard Monte Carlo uses a fixed number of runs with no guarantee on estimation quality. MultiVeStA applies sequential statistical model checking: it runs simulations adaptively, stopping only when the 95% confidence interval on E[logGDP] is narrower than δ = 0.05 at every time step. This provides a formal precision guarantee — the sample size is determined by the data, not by the experimenter.


Parameter Explorer

Interactive Sensitivity Analysis

Run MultiVeStA analysis interactively. Select a parameter, choose values to compare, and watch the sequential sampling converge. Select a parameter, choose values, and watch MultiVeStA's sequential sampling converge in real time.

// Select a parameter and values, then click Run

AGR peaks at ε ≈ 0.1: moderate exploration maximises long-run growth. Zero exploration → stagnation. Full exploration → wasted effort.


Key Findings

Results & Statistical Validation

6/7
Counterfactuals significant
Welch t-test at every timestep. Only ρ=3.0 vs ρ=5.0 reveals saturation.
ε≈0.1
Optimal exploration rate
Confirmed via AGR sweep — robust finding from Fagiolo & Dosi (2003).
δ=0.05
Formal CI guarantee
MultiVeStA auto-selects sample size — no arbitrary fixed run count.

Convergence (δ=1) is governed by output variance. Only low-variance regimes converge within δ=0.05.

The refactored MATLAB model reproduces all stylized facts of Fagiolo & Dosi (2003).

Ribbons = 95% CI  ·  Baseline: ε=0.1 shows sustained growth  ·  Stagnation: ε=0 plateau confirms exploration is necessary for long-run growth.


Replicability

Code & Replicability Package

  • 📁 Model2.m — Main MATLAB model (218 lines)
  • 📁 Agent.m — Agent class
  • 📁 AGR.m — Average Growth Rate
  • 📁 *.multiquatex — MultiVeStA queries
  • 📁 mvMatlab.jar — MultiVeStA engine (Java)
  • 📁 run.sh — One-click sweep launcher
  • 📁 plot_*.py — Result visualisation scripts
logGDPaftersteps.multiquatex
eval obsAtStep(x; logGDP) in [1..201 step 10]
with confidence 0.95 and delta 0.05;
AGRfinal.multiquatex
eval obsAtStep(201.0; AGR_total)
with confidence 0.95 and delta 0.05;
🔬 MultiVeStA on GitHub