Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking (Artifact)

Artifact for Paper Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking (Artifact) accepted for FM 2026.The artifact contains the two multi-objective probabilistic model checking tools mcsta (part of The Modest Toolset) and Storm using a multi-platform Docker image for convenient installation.Benchmark models and benchmarking scripts are provided to reproduce all experiments from the paper.A representative subset of experiments is included to assess reproducibility in reasonable time.