Distributed Statistical Model Checking for Discrete Event Simulators

MultiVeStA query and plot

A property in the simulator-independent query language of MultiVeStA, and the obtained plot.


MultiVeStA is an efficient statistical analysis tool which can be easily integrated with existing discrete event simulators, enriching them with distributed Statistical Analysis and Statistical Model Checking capabilities.

The tool originally focused on transient-time analysis, but it has recently been enriched also with steady-state (or long-run) analysis capabilities. Please check here for further details on the latter.

The tool is maintained and developed by Stefano Sebastio and Andrea Vandin. The tool extends the existing VeStA and PVeStA tools.

Download MultiVeStA, and contact us for guidelines on using it.

Supported Simulators (in alphabetic order):

  • Alchemist: a simulator targeting chemical-oriented computational systems
  • ARGoS: a multi-robot, multi-engine simulator for heterogeneous Swarm robotics
  • Bike Sharing Simulator — TopoChecker topological model checker: A Tool-chain for Statistical Spatio-Temporal Model Checking of Bike Sharing Systems
  • Bio-PEPA: a language for the modelling and the analysis of biochemical networks
  • CO2: A Contract-Oriented middleware
  • DESMO-J: a framework for discrete-event modeling and simulation (contributor Claudia Cauli)
  • DEUS: a general-purpose, open-source, simulator for the analysis of large scale systems
  • Edinburgh Bus Simulator: a tool for the analysis of public transportation systems
  • ERODE: Evaluation and Reduction of Ordinary Differential Equations
  • QFLan: a probabilistic feature-oriented language with quantitative constraints for product families
  • MISSCEL: an interpreter and simulator for the Service Component Ensemble Language
  • ONE: the Opportunistic Network Environment discrete event simulator (details on integration and contributors are provided here)
  • OnPlan: a framework for simulation-based online planning
  • Probabilistic Maude: an engine to execute probabilistic rewrite theories. Try out MultiVeStA with an implementation of a dice in PMaude
  • Any Python simulator, using Py4J
  • A built in DTMC and CTMC engine
  • other simulators coming soon
  • …and yours with just few lines of code (just contact us!).

Our papers on MultiVeStA

Papers by OTHERS using MultiVeStA

Other related papers


Our work is developed within and supported by the European projects QUANTICOL 600708, and ASCENS 257414.

We are grateful to the proposers of (P)VeStA, our starting point: Gul Agha, Musab Alturki, José Meseguer, Koushik Sen and Mahesh Viswanathan.

Furthermore, we thank the main author of Alchemist (Danilo Pianini), who provided valuable help and suggestions to improve MultiVeStA, as well as Benjamin Byholm, who helped us in extending the support of MultiVeStA to python simulators. We also thank Stephen Gilmore and Mirco Tribastone, for their help in integrating MultiVeStA with BioPEPA.

Last but not least, we thank Michele Amoretti and Alberto Lluch Lafuente, who supported and suggested this work from the very beginning.



For suggestions, remarks, bugs, or to have more information about the usage of MultiVeStA, or about its integration with a simulator, please do not hesitate to contact: