MC2MABS

MC2MABS: A Monte Carlo Model Checker for MultiAgent-Based Simulations

Motivation

With their ability to produce complex, emergent behaviour from the action and interaction of its components, agent-based simulations are notoriously difficult to understand and to engineer. In the multiagent systems community, formal and semi-formal verification approaches (both qualitative and quantitative) have shown great power. Methods and tools for the verification of agent-based simulations in particular, however, are still largely missing. With potentially large populations, different observational levels, heterogeneity, a strong focus on emergent behaviours, and a significant amount of randomness, agent-based simulations possess a range of characteristics which, in their combination, represent a great challenge for verification.

MC2MABS, the Monte Carlo Model Checker for MultiAgent-Based Simulations, is tailored to the analysis of large-scale stochastic simulation models. It is designed as a tool framework that incorporates the idea of statistical runtime verification (SRV), a combination of runtime verification and statistical model checking. The central characteristic of the tool is the interleaving of simulation and property evaluation which allows for the verification of arbitrary existing simulation models, irrespective of their underlying programming language.

Each execution of a stochastic simulation model produces a random trace through the underlying state space. By verifying a property on a sufficiently large number of simulation traces, its probability can thus be estimated to an arbitrary level of precision. Clearly, the usefulness of this idea is critically dependent on the number of traces analysed. As a consequence, the efficiency of each trace check can be improved significantly by interleaving simulation and verification. As opposed to formal macro-level analysis, SRV preserves the individual richness of the ABS and allows for the verification of interesting properties in a semi-formal way. Due to its focus on independent traces, SRV is easily parallelisable and thus highly scalable by exploiting the power of modern parallel hardware.

MC2MABS is a practical framework that is based on four central requirements:

  1. efficiency: timely and tunably accurate verification of large-scale simulation models,
  2. expressivity: formulation and verification of qualitative and quantitative correctness properties in a formal, rigorous way,
  3. flexibility: verification of arbitrary simulation models, and
  4. immediacy: verification of the simulation model itself, not an abstract,  simplified model thereof.
Design rationale

When designing a framework for the verification of existing simulation models, one of the biggest challenges is to cope with the heterogeneity of simulation platforms. Many simulation environments are written in Java (e.g. Repast, Mason) or in a JVM-based languages such as Scala (e.g. NetLogo); others are written in C++ (e.g. Argos, Omnet++), or in Python (e.g. MESA, SimPy), to name but a few. Rather than focussing on one or several of those languages exclusively, we decided to make MC2MABS as generic as possible and decouple the implementation of the verification mechanism from the interface to the underlying simulation model. This design allows for the integration of arbitrary simulation models, irrespective of their underlying programming language.

Architecture
Basic architecture of MC2MABS

In order to achieve the goal of independence, MC2MABS has been designed as a client-server application that consists of two layers: a verification layer and an adapter layer.

As the name suggests, the verification layer is responsible for the verification of a given temporal logic property on a trace produced by the underlying simulation. The central component in the verification layer is the monitor which implements an online verification algorithm (for further information, check out [1] and [2]).

The purpose of the adapter layer is to abstract away from the underlying simulation model through a set of well-defined callback functions. Those callback functions encapsulate the calls to the actual simulation model. From the perspective of monitor, the adapter layer thus provides a unified interface to the underlying simulation models.  In order to facilitate communication with the simulation model, the adapter is written in the target programming language and communicates with the simulation model via direct method calls (e.g. using a dedicated API). Communication between the adapters and the verification layer happens via a lightweight network interface using ZeroMQ. This achieves the desired decoupling between the verification algorithm and the underlying simulation. In general, communication between the simulation and the monitor is kept to a minimum — only information that is strictly required for verification is transferred between the two layers. This helps to keep them largely separated and to reduce design dependencies.

Implementation

The verification layer is implemented in Haskell and C.
It consists of the following three logical modules:

A sequence diagram of the verification process
A sequence diagram of the verification process
  1. MC2MABS: represents the central component; collects configuration information and triggers the verification.
  2. Evaluation: performs the manipulation of logic-independent obligations and triggers setup and teardown of the underlying simulation.
  3. SimLTL: contains logic that is tailored to simLTL, the property specification language contained in simLTL; performs verification of basic simLTL expressions and triggers the verification of agent and population properties in the underlying simulation model.

As described above, the verification layer communicates with the adapter layer via ZeroMQ messages. The adapter layer communicates with the actual simulation model by means of method calls. The overall process is illustrated graphically in the sequence diagram on the right.

 

Download

The latest version of MC2MABS can be downloaded from GitHub here.


References

[1] Herd et al.: MC2MABS: A Monte Carlo Model Checker for Multiagent-Based Simulations, B. Gaudou, J. S. Sichman (Editors): Multiagent-based Simulation XVI, Lecture Notes in Computer Science (LNCS), pp 37-54, 2015, ISBN: 978-3-319-31446-4

[2] Herd et al.: Monitoring hierarchical agent-based simulation traces, G. Weiss, P. Yolum, R. Bordini and E. Elkind (Editors): International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2015), Istanbul, Turkey, 2015, ISBN: 978-1-4503-3413-6