dtControl2+epsilon

dtControl2+ϵ TACAS 2026 paper 9769 Jan Křetínský, Tobias Meggendorfer, Sabine Rieder, and Maximilian Weininger Artifact Description This artifact contains all the code and data necessary for replicating the experiments described in the tool paper “dtControl2+ϵ: Trading Optimality for Explainability in MDP via Decision Trees”. The artifact includes a ready-to-use Docker image. Moreover, we provide the source code, Dockerfiles, and instructions to (re-)use and modify our tool. Building the Docker image from sources is not required for the evaluation. It is only included for completeness and future availability. Together, we believe that our artifact is reusable; we provide detailed justification in the section “Reusability Criteria” at the end of the document. Since submitting the paper, we have further improved the code, particularly focusing on efficiency and some corner cases. Therefore, some results, especially runtime, might be slightly better. Quickstart The “Evaluation” section provides a brief sequence of commands necessary to set up and replicate the experiments, as well as guidance on interpreting the results. Further explanations, such as the structure of the artifact and code, are provided in the subsequent sections. Artifact Requirements Hardware For minimal results, the artifact only requires modest hardware (a single CPU core and ideally 16GB of RAM – but less would also work). For complete results, we recommend access to a larger machine (ideally 20+ cores and 320+ GB RAM), as otherwise replicating results in the main part of the paper may require up to 120 hours. The artifact was tested on a Lenovo ThinkPad with an Intel i7-8565U CPU, 16 GB RAM, and Ubuntu 24.04 and a server with an AMD EPYC 9274F CPU, 404 GB RAM, and Debian GNU/Linux 12. Software On the host machine, we only require Docker or Podman. Time Without changes, the evaluation runs for approximately 8 hours on the server when only recomputing parts of the main body of the paper, and an additional 14 hours for Table 4, which requires replication of the dtNest settings. This amount of time is necessary to obtain sensible results: Our evaluation considers 38 different experiments with large underlying MDPs and 40 configurations for each of them. We provide a simple way to reduce the overall runtime by restricting to 9 experiments and excluding the comparison to dtNest. This simple run is suitable for consumer hardware and sufficient to replicate the main findings of the paper. Evaluation Part 1: Setup & Smoke Test # Load the Docker image docker load -i dtcontrol2epsilon.tar 1 # Make a folder to store the results in mkdir results # Run the Docker and mount the folder docker run -it --rm -v ./results:/workspaces/dtcontrol-epsilon/results \ dtcontrol2epsilon:latest bash # Run the following inside the Docker # Smoke test -- evaluate the example from Figure 1 python /workspaces/dtcontrol-epsilon/main.py \ --model /workspaces/dtcontrol-epsilon/models/tinyrobot.prism \ --const "" --property 'Pmax=? [ ((!"dead") U "repair")]'\ --exp-name tinyrobot build \ --export-dot /workspaces/dtcontrol-epsilon/results/tinyrobot/tiny.dot \ --precision 0.001 --heuristic simulation \ --dataset controller --noguards # Create the dot image dot -Tpng ./results/tinyrobot/tiny.dot \ -o ./results/tiny.png If these commands finish without error, the smoke test passed. Obtained results are stored in the folder results/tinyrobot . In particular, the folder contains a dot file (also rendered to a image) showing the decision tree for the tinyrobot example. Part 2: Full evaluation The following steps assume that the user is in a bash-like terminal inside the root folder of the artifact and that docker is installed. Running on Consumer Hardware To start the full evaluation, please start the Docker: mkdir results_experiments docker run -it --rm \ -v ./results_experiments:/workspaces/dtcontrol-epsilon/results_experiments \ dtcontrol2epsilon:latest bash Inside the Docker run the command below. ./run_small.sh Running on a Server For running the complete evaluation on a server, parallel (https://linux.die.net/man/1/parallel) is required. Before running on the server, please create a directory for the containers to mount and to store the logs: mkdir results_experiments To run the experiments from the main body of the paper, execute the following script outside the container. This evaluation requires a machine with 20 CPUs and at least 320GB of RAM. (If your machine has fewer CPUs or cores, adapt the value of the --jobs flag accordingly.) parallel --eta --progress --jobs 20 --delay 2\ --joblog log -a runs/run_tacas.txt To reduce the runtime of the first script by around half, restrict the run to the portfolio as follows. Note that in this case hardware restrictions still apply and the final plots will not contain a meaningful line for the virtual best. parallel --eta --progress --jobs 20 --delay 2\ --joblog log -a runs/run_tacas_portfolio.txt To combine the final results, run the following Python script, either locally or after copying all result files from results_experiments into a Docker container: 2 python ./scripts/plots_updated.py \ --result_path ./results_experiments/ To execute the benchmarks from Table 4, use the following command. Please note that this requires significant runtime and does not reproduce the results from dtNest, as we found only minor differences to those reported in their paper. Hardware restrictions apply as above. mkdir results-dtnestcomp parallel --eta --progress --jobs 6--delay 2--joblog log -a runs/run_paynt_tests_ours.txt Results can be aggregated with: python scripts/plots_updated.py \ --result_path ./results-dtnestcomp/ \ --only-main Generating the Latex Document If you have LaTeX installed, you can then compile the figures directly by running: # Produce the figures with the same TikZ code as in the paper latexmk figures.tex In case latexmk is not available, running pdflatex figures.tex two times should also produce the output PDF. In case LaTeX is not available or outdated, run: docker run -v $(pwd):/data -w /data texlive/texlive:TL2023-historic \ latexmk -pdf /data/figures.tex Note that the LaTeX file requires the results to be in a folder named results_experiments/ in its own directory. Produced Results This artifact reproduces all experimental claims of the paper, namely: •Comparison of our method to dtControl (Figure 4, page 13). •Comparison to CAV15 (Figure 5, page 13) Additionally, the artifact reproduces the following figures in the appendix: •Comparison of reduction heuristics (Table 1, page 30) •Concrete Sizes of DTs (Table 2, page 31) •DT sizes after pruning in comparison to CAV15 (Figure 7, page 32) •Runtime and DT size comparisons (Figure 8, page 32) •Detailed runtime (Table 2, page 33) The comparison to dtNest (Table 4, page 34) is provided as a CSV. It also cannot be replicated exactly, as dtNest only outputs its results via standard output. Nevertheless, the results of dtControl2+ ϵ are provided. We believe that this is sufficient, in particular as we have only found minor deviations from the previously reported results for dtNest. The figures are created by a LaTeX document ( figures.tex ), which contains the same code used to produce the figures as in the paper, allowing for direct pattern matching. Viewing and Interpreting Results All results can be seen by inspecting figures.pdf . Note that, as usual, runtimes can fluctuate, both due to varying loads on the same machine as well as differences in architectures. As such, all results based on runtime may slightly differ from those presented in the paper. Nevertheless, observe that runtime is not the primary focus of the paper anyway. For the size of DTs, note that StormPy may return different scheduler, which may influence the size of the constructed trees in some cases. Moreover, as mentioned in the introduction, we have improved the tool since submission, which may lead to smaller DTs. Finally, when running the smaller evaluation, of course, only a subset of results is produced. 3 The figures structurally match those in the paper, allowing them to be compared side by side to validate that the overall trends are similar. Results The original data obtained in our evaluation is contained in the folder results_experiments/ in the Docker container. This folder also contains aggregated files after running the whole script. Logging results are in logs/. Structure of the Artifact This artifact contains several top-level files/folders: •dtcontrol: This folder contains the (adapted) code from dtControl. •epsilon : The code required for the epsilon functionality. In particular, this contains the code for dataset construction, pruning, and adaptive learning of the tree, with feedback from the model checker. •models: All model files, either from QVBS or the evaluation from dtNest. •paynt : The code required for running dtNest. Please note that the connection to dtNest is currently not stable due to restrictions of the dtNest artifact. •runs: A collection of different evaluation runs. •scripts: The code required for postprocessing and creating the figures. •figures.tex: A LaTeX file that assembles the plots exactly as in the paper. •LICENSE.txt: The licence of dtControl+ϵ. •main.py: The main file of our tool. •plots.tex: Information on how to generate the plots. It is imported in figures.tex. •requirements.txt: The requirements needed for dtControl. •run*: Evaluation scripts for the artifact. Using dtControl+ϵ Our tool can be run in two configurations. The first one runs experiments containing all combinations of dataset types and weight heuristics. It is called experiments . The second configuration, build , runs a single combination of dataset type and weight heuristic. To run experiments, call: python main.py --model <path_to_model>\ --const "model constants" \ --property <considered_property>\ --exp-name <name_of_the_experiment>\ experiments --precision <precision_as_float> For running just a single instance, call: python main.py --model <path_to_model>\ --const "constants" \ --property "considered property" \ --exp-name <experiment_name>build The following parameters can be optionally used: •--export-dot path_to_dot: Creates a dot file as output •--export-json path_to_json: Creates a JSON file •--precision precision_as_float: allows to set a precision •--heuristic (simulation|cost_of_error|agency|uniform): selects the dataset weight heuristic •--dataset (controller|permissive|combined): selects the dataset type •--noguards: disables guard splitting •--linear: enables linear splitting •--export-statistics path_to_file: Exports information on the run •--time-solving time_in_seconds: Allows setting timeouts for solving the model •--time-building time_in_seconds : Restricts the amount of time spent on building the tree and creating the dataset (default is 10 minutes) 4 •--time-pruning: Time limit for pruning the decision tree. This can also be done using the Docker image, i.e., docker run .... Modifying dtControl2+ϵ To modify the tool, apply your modifications in the respective folders and re-build the Docker image. Reusability Criteria In this section, we outline how we satisfy each requirement of the reusability badge. Availability The artifact itself is published on Zenodo (doi: 10.5281/zenodo.17484917), the source code of dtControl2+ ϵ is freely available on GitLab. Functional Aspects • Documentation: We believe that this README explains in detail how to replicate the experiments and that the evaluation scripts are comparatively simple to understand. •Completeness: Experimental claims are supported by this artifact. •Consistent: We could replicate our results using this artifact. • Correctness & Testing: We use Strom to cross-validate the correctness of both the final result and intermediate steps. For example (with assertions enabled), we also validate that the constructed dataset is epsilon-correct by building the induced MDP and checking that the worst-case is at most epsilon away from the best-case. Reusability Aspects •Licence: The GNU General Public License v3.0 is one of the most permissive licenses. •Dependencies: The few dependencies are documented through the build script. •Usage beyond the paper: We provide instructions on how to use and modify dtControl2+ϵ. •Open source: The artifact is open source. 5