# dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts

arXiv: https://arxiv.org/abs/2101.07202 · HTML: https://mlsanity.com/paper/2101.07202/

## Key facts

- Cited by 14 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 48 references that are in the map.
- First posted on arXiv 15 Jan 2021.

## Builds on (most cited first, 10 of 10)

- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [dtControl: Decision Tree Learning Algorithms for Controller Representation](https://mlsanity.com/paper/2002.04991/) (2020)
- [Counterexample Explanation by Learning Small Strategies in Markov Decision Processes](https://mlsanity.com/paper/1502.02834/) (2015)
- [SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes](https://mlsanity.com/paper/1906.10640/) (2019)
- [SPUDD: Stochastic Planning using Decision Diagrams](https://mlsanity.com/paper/1301.6704/) (2013)
- [Strategy Representation by Decision Trees in Reactive Synthesis](https://mlsanity.com/paper/1802.00758/) (2018)
- [Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games](https://mlsanity.com/paper/1903.12576/) (2019)
- [Strategy Representation by Decision Trees with Linear Classifiers](https://mlsanity.com/paper/1906.08178/) (2019)
- [Optimal Symbolic Controllers Determinization for BDD storage](https://mlsanity.com/paper/1803.07369/) (2018)
- [Learning-Based Synthesis of Safety Controllers](https://mlsanity.com/paper/1901.06801/) (2019)

## Built on by (most cited first, 14 of 14)

- [Algebraically Explainable Controllers: Decision Trees and Support Vector Machines Join Forces](https://mlsanity.com/paper/2208.12804/) (2022)
- [1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization](https://mlsanity.com/paper/2410.18293/) (2024)
- [Learning Explainable and Better Performing Representations of POMDP Strategies](https://mlsanity.com/paper/2401.07656/) (2024)
- [Formally Verifying and Explaining Sepsis Treatment Policies with COOL-MC](https://mlsanity.com/paper/2602.14505/) (2026)
- [Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking](https://mlsanity.com/paper/2511.08078/) (2025)
- [In Search of Trees: Decision-Tree Policy Synthesis for Black-Box Systems via Search](https://mlsanity.com/paper/2409.03260/) (2024)
- [Taming Infinity one Chunk at a Time: Concisely Represented Strategies in One-Counter MDPs](https://mlsanity.com/paper/2503.00788/) (2025)
- [Explaining Control Policies through Predicate Decision Diagrams](https://mlsanity.com/paper/2503.06420/) (2025)
- [Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems](https://mlsanity.com/paper/2508.16345/) (2025)
- [Explainable Representation of Finite-Memory Policies for POMDPs using Decision Trees](https://mlsanity.com/paper/2411.13365/) (2024)
- [COOL-MC: Verifying and Explaining RL Policies for Platelet Inventory Management](https://mlsanity.com/paper/2603.02396/) (2026)
- [Explainably Safe Reinforcement Learning](https://mlsanity.com/paper/2606.04634/) (2026)
- [dtControl2+varepsilon: Trading Optimality for Explainability in MDPs via Decision Trees](https://mlsanity.com/paper/2607.25925/) (2026)
- [Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle](https://mlsanity.com/paper/2608.30581/) (2026)

## Abstract (arXiv)

Recent advances have shown how decision trees are apt data structures for concisely representing strategies (or controllers) satisfying various objectives. Moreover, they also make the strategy more explainable. The recent tool dtControl had provided pipelines with tools supporting strategy synthesis for hybrid systems, such as SCOTS and Uppaal Stratego. We present dtControl 2.0, a new version with several fundamentally novel features. Most importantly, the user can now provide domain knowledge to be exploited in the decision tree learning process and can also interactively steer the process based on the dynamically provided information. To this end, we also provide a graphical user interface. It allows for inspection and re-computation of parts of the result, suggesting as well as receiving advice on predicates, and visual simulation of the decision-making process. Besides, we interface model checkers of probabilistic systems, namely Storm and PRISM and provide dedicated support for categorical enumeration-type state variables. Consequently, the controllers are more explainable and smaller.