**SALMA** (Simulation and Analysis of Logic-Based Multi-Agent Models) is a new approach for *simulation and statistical model checking of multi-agent system models*.

Different from existing methodologies, the mechanics of the simulated system are specified by means of logical axioms based upon the well-established *situation calculus*. Leveraging the resulting first-order logic structure of the system model, the simulation is coupled with a statistical model-checker that uses a first-order variant of time-bounded linear temporal logic (LTL) for describing properties. This creates a very expressive framework for modeling and verification that allows direct fine-grained reasoning about the agent’s interaction with each other and with their (physical) environment.

The source code for the SALMA toolkit, including some examples, can be retrieved from GitHub:https://github.com/salmatoolkit/salma