ULTIMATE v1.1 - A Tool for the Verification and Synthesis of Stochastic World Models (with Supplementary Material)

Overview This artifact provides the virtualised environment and source code for ULTIMATE, a tool for the verification and synthesis of stochastic world models, as presented in the paper "ULTIMATE: A Tool for the Verification and Synthesis of Stochastic World Models" (CAV 2026), alongside a README file with detailed evaluation instructions, and a copy of its licence (GNU General Public License v3.0 - GPLv3). This version of the record (v1.1 with Supplementary Material) includes a PDF document providing additional definitions, proofs, model details, and experimental data supporting the main publication. ULTIMATE is designed to handle the compositional verification and correct-by-construction synthesis of stochastic world models—heterogeneous networks of interdependent stochastic models including discrete and continuous-time Markov chains, Markov decision processes (MDPs), partially observable MDPs, and stochastic multi-player games. Throughits unique integration of multiple probabilistic and parametric model checking paradigms, our tool unifies the modelling, verification and synthesis of systems characterised by a combination of probabilistic and nondeterministic uncertainty, discrete and continuous-time behaviour, partial observability, and multi-agent interaction. This VM ensures long-term reproducibility by providing a pre-configured environment where all dependencies are already configured and integrated. Included Content Supplementary Material (PDF): Provides additional definitions, formal proofs, detailed model specifications, and further experimental data. ULTIMATE Tool (v1.1): The full Java-based GUI and Command-Line Interface. Case Studies: A comprehensive suite of models (DTMCs, CTMCs, MDPs, POMDPs, and SMGs) supporting the results in the CAV paper: Verification: RAD, SMD, DPM-FX, RoboFleet, and RoCo case studies. Synthesis: SmartFarming, RAD-synth, and Casino case studies. Scalability: Synthetic stochastic world models based on DPM-FX, and several of the largest models from the PRISM benchmark suite. Dependencies: Pre-installed versions of PRISM, PRISM-games, Storm, SciPy, EvoChecker, and the Java Runtime Environment (JRE). Documentation: README with detailed evaluation instructions, and a 4-minute demonstration video (embedded in the VM). Further instructions are available in the project GitHub (https://github.com/ULTIMATE-YORK/ULTIMATE). LICENCE: GNU General Public License v3.0 (GPLv3). VM Technical Specifications Format: OVA (Open Virtualization Format) Guest OS: elementary OS (Ubuntu-based) User Credentials: user / user Specification: 8GB RAM and 2 CPU cores. Architecture: This appliance is built for x86_64 (Intel/AMD) processors.