Pith. sign in

REVIEW 2 major objections 4 minor 79 references

dtControl2+$\varepsilon$: Trading Optimality for Explainability in MDPs via Decision Trees

T0 review · 2 major / 4 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A small, user-chosen allowance of imprecision ε makes decision-tree controllers for Markov decision processes orders of magnitude smaller, while a model-checking loop certifies that every returned tree stays within ε of the optimal value.

desk verdict Credible tool paper with a real ε-optimality theorem and strong empirical results; the practical guarantee leans on Storm's numerics more than the proof admits. read the letter →

arxiv 2607.25925 v1 pith:DXN64TPD submitted 2026-07-28 cs.AI

Tereza Kinská , Jan Křetínský , Tobias Meggendorfer , Sabine Rieder , Maximilian Weininger This is my paper · ORCID
classification cs.AI
keywords decisiontreesMarkovprocessescontrollersynthesisepsilon-optimalityexplainabilityprobabilisticmodelcheckingpermissivecontrollerspolicycompression
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Markov decision processes get their controllers from synthesis tools as huge tables of state-action pairs; decision trees make them readable, but even trees from the current state-of-the-art tool are too large for humans once the system has many corner cases. This paper's claim is that the size problem is mostly unnecessary: if the user allows a small, specified error ε, most decisions can be dropped, and a decision tree capturing only the decisions that matter is enough, with its performance guaranteed to be within ε of optimal. The tool dtControl2+ε couples decision-tree learning with a probabilistic model checker: safe reductions delete states whose choices cannot influence the outcome by more than ε, and aggressive shrink steps (simulation-weighted learning, early stopping, pruning) are each verified by model checking and backed off if they break the guarantee. On 38 standard benchmarks the resulting trees are at least as small as, and often orders of magnitude smaller than, those of prior tools, and at ε=0.01 nearly half the benchmarks collapse to a single rule: one action (with random fallback when unavailable) is already ε-optimal. If correct, this gives controller design a genuine explainability dial — the user picks the error budget and receives a certified, human-readable rule.

What carries the argument

The load-bearing mechanism is the permissive dataset plus a verification loop. Rather than learning a tree from one optimal controller (one action per state), the tool builds a dataset assigning each state a set of allowed actions so that every controller consistent with it is provably ε-optimal (Theorem 1). Safe reductions delete states — AllOpt (all actions equally good), Agency (best-vs-worst value gap ≤ ε), Dominance (another state reached with probability 1 regardless of choice), Unreach (never reached from the start) — while keeping the ε-claim. Greedier steps (simulation-weighted learning, early stopping, pruning) may break the guarantee, so each candidate tree is model-checked and th

What would settle it

On a benchmark where the tool aborts at ε=0 because the model checker's returned controller was confirmed non-optimal (e.g., consensus4-4-c2 or zeroconf-1000-2-false-correctmax), compute the true optimal value with an independent exact-arithmetic solver, then model-check the tree the tool outputs at ε=1e-6; if the true gap exceeds 1e-6, the ε-optimality guarantee is broken. The paper supplies the ingredients for this test: its own second model checking query disagreed with the first by more than 10^-14 on those benchmarks.

Watch

Extended reading notes

Core claim

On its own terms, the paper establishes a guarantee and an empirical fact. The guarantee: given any MDP, any standard objective (reachability, safety, reach-avoid, expected reward, LTL with memory), and any precision ε ≥ 0, the tool returns a decision tree T with |V^T(s̄) − V(s̄)| ≤ ε — the tree's value at the initial state is within ε of optimal; ε=0 recovers an exact optimal controller. The empirical fact: on 38 benchmarks the trees beat all four competitors, more than two orders of magnitude smaller than the previous tool on 12 of 38, and at ε=1e-2 produce trees of at most 15 nodes on 30 benchmarks and single-node trees on 18 — in nearly half the benchmark systems, always playing one fixe

Load-bearing premise

The whole guarantee rests on the model checker computing exact optimal values: the verification loop that certifies ε-optimality compares the candidate tree's value with the solver's own optimum, and the appendix reports ε=0 runs where the solver's 'optimal' controller was provably not optimal (differing by more than 10^-14 between two queries) — so if the solver's numerical error exceeds the allowed ε, an output tree can violate its certificate without the tool detecting it.

Editorial extensions

If this is right

  • The user can dial a single parameter ε and receive a certified bound on the controller's suboptimality, so the simplicity/performance trade-off becomes explicit and auditable rather than a gamble on a pruning heuristic.
  • The single-node results at ε=1e-2 imply that many standard benchmark MDPs do not actually need a complex policy: a fixed action with uniform random fallback is within 1% of optimal, a structural fact about the models that exact controller synthesis had hidden.
  • The guarantee transfers across the full objective spectrum — reachability, safety, reach-avoid, expected reward/cost, and LTL with memory (the only tool in its class with LTL support) — so the same ε-optimal simplification applies in each of these settings.
  • Even at ε=0 the pipeline is strictly better than the predecessor tool on every benchmark, by more than two orders of magnitude on 12 of 38 — the permissive dataset, safe reductions, and automatic predicates improve exact representation too.
  • Because the verification loop certifies the final tree, future aggressive heuristics can be added without endangering correctness: if they produce an ε-violating tree, the tool detects it and relaxes them.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A cheap complexity probe suggests itself: run the pipeline at a coarse ε (say 1e-2) before committing to full synthesis; if the result is one or a few nodes, the system's apparent decision complexity is not load-bearing for the specification, and the remaining work in building and maintaining a detailed controller may be unnecessary.
  • The reduced dataset size (after safe reductions) could serve as a definition of an MDP's decision complexity per se, separating 'hard' systems from merely 'large' ones — a distinction the paper itself notes indirectly when observing no correlation between model size and runtime.
  • For ε near the solver's numerical noise floor, a practical hardening would run the verification loop with exact rational arithmetic: the certifier, not the learner, is what must be made exact, and the paper's appendix shows ε=0 cases where the solver's own two query results disagreed beyond floating-point precision.
  • The permissive-dataset formulation points toward a transfer route for parameterised model families: a tree certified on one instance could be checked and locally patched on nearby instances, turning per-instance compression into a reusable rule.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper presents dtControl2+ε, an extension of dtControl2 that constructs decision-tree controllers for MDPs with a formal ε-optimality guarantee. The workflow solves the MDP with Storm, constructs a permissive/reduced dataset of 'relevant' decisions, learns and prunes a DT, and validates the result by model checking. The central Theorem 1 states that the dataset construction and reductions are ε-optimal; the appendix contains a proof. Empirically, on 38 PRISM benchmarks the tool reports substantially smaller DTs than dtControl2, dtPaynt, dtNESt, and CAV15, including single-node DTs for 18 benchmarks at ε=1e-2. The paper also documents that on several ε=0 benchmarks Storm returned a controller that was not optimal and the tool aborts.

Significance. If the guarantee is delivered, this is a notable advance: it provides tunable explanations for MDP controllers with a formal bound, covers standard objectives, and has a reproducible artifact. The proof of Theorem 1 is a genuine effort, and the evaluation is extensive with full tables. The main caveat is that the practical guarantee depends on numerical exactness of Storm. Since the paper itself reports failures of that exactness, the advertised absolute guarantee is currently too strong. With a clarified assumption or a certified downstream check, the contribution would be solid.

major comments (2)
  1. [§III Problem Statement and §III-C; Appendix E3/E4] The paper states: 'Given an MDP, objective, and precision ε≥0, obtain a (small) decision tree T such that |V^T(¯s)-V(¯s)| ≤ ε.' Appendix E3/E4 reports that for several ε=0 benchmarks the controller obtained from Storm 'was not optimal, as confirmed through a second model checking query; it also differed by more than the float precision of 10^-14', and the tool aborts. Thus the claim as stated is false for the implemented tool. Theorem 1's proof assumes the initial dataset is built from a truly optimal controller. Please either (a) restrict all claims to the case where Storm's oracle is exact, or (b) provide a certified exact solving/validation path that justifies the absolute statement.
  2. [§III-C verification loop] The verification step compares the DT's value against Storm's computed optimal value, both produced by Storm. If Storm's optimal value has numerical error δ > 0, a DT whose true error is ε+δ can pass the check. The paper gives no bound on δ and indeed documents numerical inexactness in Appendix E3/E4. This is not a remote edge case: the same solver is used both to construct the dataset and to validate the DT. Please add a numerical error analysis or an external exact checker, or at minimum explicitly state that the guarantee is relative to Storm's arithmetic.
minor comments (4)
  1. [§III] The statement 'if a decision tree exists, our tool will always find one by omitting aggressive heuristics when necessary' is not justified by Algorithm 1, which is a greedy heuristic with a fixed predicate set. If the dataset contains states with identical feature values but different required actions, no axis-aligned split can separate them. Please either weaken this claim or provide a proof.
  2. [Appendix E3/E4] The sentence 'Even though we set Storm to sound solving, we were not able to avoid such cases. In these cases, dtControl 2+ε aborts.' appears verbatim in both E3 and E4. Please remove the duplication and clarify whether the abort is triggered by the second model-checking query or by an exception.
  3. [§V-B] For Imp_Simulation and Imp_CoE, the text says that adding a small positive weight 'ensures ε-optimality'. A small weight by itself does not guarantee the bound; the final model-checking step is what enforces it. Please rephrase to avoid the implication that the weighting alone is sufficient.
  4. [Appendix A] The LTL support is described as a differentiator, but the appendix admits that memory states are opaque numbers and that no LTL benchmarks are evaluated. Please label this as preliminary and provide at least the hand-crafted instances or a clear statement that LTL is not part of the experimental comparison.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular reduction found; the ε-optimality guarantee is derived from standard MDP arguments and an external published certificate, not from fitted benchmark values.

full rationale

The paper's central correctness claim (Theorem 1, Appendix D) is not built by fitting or by defining the target in terms of the output. Lemma 1 and Lemma 2 are proved in the appendix from MDP semantics. The permissive initial dataset construction relies on [20]'s fixed-point certificate (used as Lemma 3); although [20] shares an author with this paper, it is an externally published TACAS result with stated assumptions that do not include the current benchmarks, and the paper reproduces the argument rather than merely citing it as a uniqueness theorem. No benchmark constant or measured DT size is fed back into the derivation, and ε is an input, not a fitted parameter. The tool's final model-checking step is a verification oracle, not a fitted source of the claimed guarantee. The appendix's admission that on some ε=0 instances Storm's controller 'was not optimal, as confirmed through a second model checking query; it also differed by more than the float precision of 10^-14' is a real numerical-correctness risk, but it is a limitation of the external oracle, not a circular step in the derivation. Accordingly, no circularity step is warranted.

Assumptions & free parameters 3 free parameters · 5 assumptions · 1 invented entities

The central guarantee is built on standard MDP semantics plus external certificate results; there are no fitted scientific parameters, but several heuristic constants (θ, 1e-6 weight) and toolchain assumptions enter the practical pipeline.

free parameters (3)
  • Early-stopping threshold θ = 0.5, decremented by 0.1 until success (min 0.0)
    Controls how impure a node may be before becoming a leaf; chosen for efficiency and does not affect final correctness because the verification loop checks.
  • Importance weight floor for Imp_Simulation = 1e-6
    Added to unsampled states so the dataset remains ε-optimal; arbitrary small constant.
  • Unspecified small positive weight in Imp_CoE = not given
    Paper says 'we add a small positive weight to all states' (§V-B) but does not specify value; implementation detail affecting trees.
assumptions (5)
  • domain assumption Storm returns a truly optimal controller and exact model-checking values for the MDP/objective.
    Needed in Steps 1 and 3; contradicted on some ε=0 benchmarks as admitted in Appendix E3/E4.
  • domain assumption GoodActions correctness follows from Chatterjee et al. [20, Prop. 5 and Section 3].
    Lemma 3 in Appendix D delegates proof to this external certificate result; overlapping authors but independent publication.
  • domain assumption Lemma 1: mixture of ε-optimal actions preserves ε-optimality, including when a state is revisited infinitely often.
    Proof is sketched for reachability and asserted for reward objectives; relies on objective-specific progress/reward structure.
  • ad hoc to paper For LTL, extending states with memory-state pairs preserves ε-optimality and produces interpretable DTs.
    Asserted in Appendix A with no proof; interpretability itself is doubted by authors due to opaque memory-state numbering.
  • domain assumption PRISM guard expressions are good candidate predicates for DT splits.
    §V-A; valid only when a high-level PRISM description is available.
invented entities (1)
  • Unif special leaf label
    purpose: Allows the decision tree to output 'choose one of the available actions uniformly at random' instead of a concrete action, unifying states with equal action values without losing progress.
    Introduced in §II-B/§IV-A; not an external physical entity; Remark 1 notes it assumes the runtime can pick a random available action.

how reviews work

0 comments
Cite this review

Pith. "Pith review of dtControl2+$\varepsilon$: Trading Optimality for Explainability in MDPs via Decision Trees." pith.science (2026). https://pith.science/paper/DXN64TPD

@misc{pith2026260725925,
  author       = {Pith},
  title        = {Pith review of: dtControl2+$\varepsilon$: Trading Optimality for Explainability in MDPs via Decision Trees},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DXN64TPD}},
  note         = {Machine review of arXiv:2607.25925}
}
abstract

Over the past decade, decision trees have been used to represent controllers (a.k.a. policies) in an explainable way, with dtControl2 as a current state-of-the-art tool. However, for systems that are large or have many corner cases, even such representations tend to be too complex and not human-comprehensible. Unfortunately, reducing the size of the decision tree is not straightforward, as missing just a single crucial case might result in an incorrect controller. We tackle this issue in the setting of Markov decision processes, extending dtControl2 by "$\varepsilon$" functionality: Given an allowed imprecision $\varepsilon \geq 0$, we construct a smaller decision tree, distilling the essence of the controller, while still guaranteeing its $\varepsilon$-optimality. This enables us to provide tunably simpler explanations, omitting a controllable amount of detail. Our tool constructs decision trees that are orders of magnitude smaller than the state of the art.

Figures

Figures reproduced from arXiv: 2607.25925 by the authors.

Figure 1
Figure 1. Visualisation of a grid-world robot navigation task (left) and [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Structural overview of dtControl 2+ε. The tool builds a DT representing an ε-optimal controller for an MDP. Given the model description, objective, and precision, our tool calls Storm (Ë) [36] to build the model and obtain the optimal value and controller. This controller is transformed into a reduced dataset of relevant decisions using our, in the DT-learning context novel, “safe” methods preserving the value of th… view at source ↗
Figure 3
Figure 3. MDP illustrating permissive strategies. DT to “unify” states which otherwise have disjoint sets of allowed actions, as follows: In the example, Unif is added for both states, i.e. D = {s → {l,Unif}, t → {r,Unif}}, and thus there is a consistent one-node DT, recommending Unif. Note that explicitly adding Unif is different from setting D(s) = A(s) or removing s from D: In the latter two cases, the constructed DT T may… view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: Quantile plot comparing the DT size of different configurations of [PITH_FULL_IMAGE:figures/full_fig_p009_4.png]
Figure 5
Figure 5. Figure 5: Comparison of dtControl 2 and dtNESt to our methods. The quantile plot compares the size of the final DT of dtControl 2 and dtNESt to the best DTs of dtControl 2+ε with different precision requirements. The y-axis uses logarithmic scale. DTs are always at least as smal…
Figure 6
Figure 6. Figure 6: CSMA/CD (N=2, K=6) DTs produced by dtControl 2+ε. Left: ε = 10−6 , right: ε = 10−2 . insight that is invisible to dtControl 2. Recall that in states not covered by the DT actions are chosen randomly. Pnueli-Zuck randomized mutual exclusion (n=5) [35, 62] models n proce…
Figure 7
Figure 7. Figure 7: Complete DT (left) and reduced DT (right) learnt for the optimal controller of the example in Section [PITH_FULL_IMAGE:figures/full_fig_p015_7.png]
Figure 8
Figure 8. Figure 8: DT sizes comparing dtNESt with the best of dtControl 2+ε. 18 [PITH_FULL_IMAGE:figures/full_fig_p018_8.png]
Figure 10
Figure 10. Figure 10: DT size comparison between dtNESt and the dtControl 2+ε portfolio. While dtNESt always uses ε = 0, dtControl 2+ε is shown with ε = 0 (top left), ε = 10−6 (top right) and ε = 10−2 (bottom). 19 [PITH_FULL_IMAGE:figures/full_fig_p019_10.png]
Figure 11
Figure 11. Figure 11: Comparison of runtime and DT size in relationship to the [PITH_FULL_IMAGE:figures/full_fig_p020_11.png]
Figure 12
Figure 12. Figure 12: Runtime comparison between dtNESt and the dtControl 2+ε portfolio. While dtNESt always uses ε = 0, dtControl 2+ε is shown with ε = 0 (top left), ε = 10−6 (top right) and ε = 10−2 (bottom). 21 [PITH_FULL_IMAGE:figures/full_fig_p021_12.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

79 extracted references · 22 canonical work pages

  1. [1]

    In: TOOLympics@ETAPS

    Andriushchenko, R., Bork, A., Budde, C.E., ˇCeška, M., Grover, K., Hahn, E.M., Hartmanns, A., Israelsen, B., Jansen, N., Jeppson, J., Junges, S., Köhl, M.A., Könighofer, B., K ˇretínský, J., Meggendorfer, T., Parker, D., Pranger, S., Quatmann, T., Ruijters, E., Taylor, L., V olk, M., Weininger, M., Zhang, Z.: Tools at the frontiers of quantitative ver- if...

    2023

  2. [2]

    In: Cussens, J., Zhang, K

    Andriushchenko, R., ˇCeška, M., Junges, S., Katoen, J.P.: Inductive synthesis of finite-state controllers for pomdps. In: Cussens, J., Zhang, K. (eds.) Proceedings of the Thirty-Eighth Conference on Uncertainty in Artificial Intelligence. Proceedings of Machine Learning Research, vol. 180, pp. 85–95. PMLR (01–05 Aug 2022), https://proceedings.mlr. press/v...

    2022

  3. [3]

    Andriushchenko, R., ˇCeška, M., Chakraborty, D., Junges, S., K ˇretínský, J., Macák, F.: Symbiotic local search for small decision tree poli- cies in MDPs. In: UAI. Proceedings of Machine Learning Research, vol. 286, pp. 132–148. PMLR (2025), https://openreview.net/forum?id= P0JNSkJtyN

    2025

  4. [4]

    In: CA V (2)

    Andriushchenko, R., ˇCeška, M., Junges, S., Macák, F.: Small deci- sion trees for MDPs with deductive synthesis. In: CA V (2). Lecture Notes in Computer Science, vol. 15932, pp. 169–192. Springer (2025). https://doi.org/10.1007/978-3-031-98679-6_8

    work page doi:10.1007/978-3-031-98679-6_8 2025

  5. [5]

    WIREs Data Min- ing Knowl

    Angelov, P.P., Soares, E.A., Jiang, R., Arnold, N.I., Atkinson, P.M.: Ex- plainable artificial intelligence: an analytical review. WIREs Data Min- ing Knowl. Discov.11(5) (2021). https://doi.org/10.1002/WIDM.1424

    doi:10.1002/widm.1424 2021

  6. [6]

    Arrieta, A.B., Rodríguez, N.D., Ser, J.D., Bennetot, A., Tabik, S., Bar- bado, A., García, S., Gil-Lopez, S., Molina, D., Benjamins, R., Chatila, R., Herrera, F.: Explainable artificial intelligence (XAI): concepts, taxonomies, opportunities and challenges toward responsible AI. Inf. Fusion58, 82–115 (2020). https://doi.org/10.1016/j.inffus.2019.12.012

    doi:10.1016/j.inffus.2019.12.012 2020

  7. [7]

    In: HSCC

    Ashok, P., Jackermeier, M., Jagtap, P., K ˇretínský, J., Weininger, M., Zamani, M.: dtControl: decision tree learning algorithms for controller representation. In: HSCC. pp. 17:1–17:7. ACM (2020). https://doi.org/10.1145/3365365.3382220

    arXiv 2020

  8. [8]

    In: TACAS (2)

    Ashok, P., Jackermeier, M., K ˇretínský, J., Weinhuber, C., Weininger, M., Yadav, M.: dtControl 2.0: Explainable strategy representation via decision tree learning steered by experts. In: TACAS (2). Lecture Notes in Computer Science, vol. 12652, pp. 326–345. Springer (2021). https://doi.org/10.1007/978-3-030-72013-1_17

    doi:10.1007/978-3-030-72013-1_17 2021

Show all 79 references
  1. [9]

    In: QEST

    Ashok, P., K ˇretínský, J., Larsen, K.G., Coënt, A.L., Taankvist, J.H., Weininger, M.: SOS: safe, optimal and small strategies for hybrid Markov decision processes. In: QEST. Lecture Notes in Computer Science, vol. 11785, pp. 147–164. Springer (2019). https://doi.org/10.1007/9...

    2019 doi

  2. [10]

    In: VMCAI (2025)

    Azeem, M., Chakraborty, D., Kanav, S., K ˇretínský, J., Mohagheghi, M., Mohr, S., Weininger, M.: 1-2-3-go! Policy synthesis for parameterized Markov decision processes via decision-tree learning and generalization. In: VMCAI (2025). https://doi.org/10.1007/978-3-031-82703-7_5

    2025 doi

  3. [11]

    MIT Press (2008), https://mitpress.mit.edu/books/principles-model-checking

    Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008), https://mitpress.mit.edu/books/principles-model-checking

    2008

  4. [12]

    In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R

    Bastani, O., Pu, Y ., Solar-Lezama, A.: Verifiable reinforcement learning via policy extraction. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems. vol. 31. Curran Associates, Inc. (...

    2018

  5. [13]

    https://doi.org/10.1145/3632935

    Batz, K., Biskup, T.J., Katoen, J.P., Winkler, T.: Programmatic strategy synthesis: Resolving nondeterminism in probabilistic programs (2023). https://doi.org/10.1145/3632935

    2023 doi

  6. [14]

    In: CA V (1)

    Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., K ˇretínský, J.: Counterexample explanation by learning small strategies in Markov decision processes. In: CA V (1). Lecture Notes in Computer Science, vol. 9206, pp. 158–177. Springer (2015). https://doi.org/10.1007/978-3...

    2015 doi

  7. [15]

    https://doi.org/10.1007/978-3-032-09524-4_7

    Brorholt, A.H., Høeg-Petersen, A.H., Jensen, P.G., Larsen, K.G., Mikuˇcionis, M., Schilling, C., W ˛ asowski, A.: Uppaal coshy: Au- tomatic synthesis of compact shields for hybrid systems (2025). https://doi.org/10.1007/978-3-032-09524-4_7

    2025 doi

  8. [16]

    In: AISoLA

    Budde, C.E., D’Argenio, P.R., Hartmanns, A.: Digging for decision trees: A case study in strategy sampling and learning. In: AISoLA. Lecture Notes in Computer Science, vol. 15217, pp. 354–378. Springer (2024). https://doi.org/10.1007/978-3-031-75434-0_24

    2024 doi

  9. [17]

    In: ISoLA (4)

    Budde, C.E., Hartmanns, A., Klauck, M., K ˇretínský, J., Parker, D., Quatmann, T., Turrini, A., Zhang, Z.: On correctness, precision, and performance in quantitative verification - QComp 2020 competition report. In: ISoLA (4). Lecture Notes in Computer Science, vol. 12479, pp....

    2020 doi

  10. [18]

    In: Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence

    Carr, S., Jansen, N., Topcu, U.: Verifiable rnn-based policies for pomdps under temporal logic constraints. In: Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence. pp. 4121–4127 (2021)

    2021

  11. [19]

    In: HSCC ’25: Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control (2025)

    Chakraborty, D., Dubslaff, C., Kanav, S., K ˇretínský, J., Weinhu- ber, C.: Explaining control policies through predicate decision dia- grams. In: HSCC ’25: Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control (2025). https://doi.org/...

    2025

  12. [20]

    In: TACAS (2)

    Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T., Zilken, D.: Fixed point certificates for reachability and expected rewards in MDPs. In: TACAS (2). Lecture Notes in Computer Science, vol. 15697, pp. 130–151. Springer (2025). https://doi.org/10.1007/978...

    2025 doi

  13. [21]

    Formal Meth- ods Syst

    Chen, T., Forejt, V ., Kwiatkowska, M.Z., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Formal Meth- ods Syst. Des.43(1), 61–92 (2013). https://doi.org/10.1007/s10703-013- 0183-7

    2013 doi

  14. [22]

    In: IJCAI

    Córdoba, F.C., Judson, S., Antonopoulos, T., Bjørner, K., Shoemaker, N., Shapiro, S.J., Piskac, R., Könighofer, B.: Analyzing intentional behavior in autonomous agents under uncertainty. In: IJCAI. pp. 372–

  15. [23]

    Costa, V .G., Pedreira, C.E.: Recent advances in decision trees: an updated survey. Artif. Intell. Rev.56(5), 4765– 4800 (2023). https://doi.org/10.1007/S10462-022-10275-5, https://doi.org/10.1007/s10462-022-10275-5

    2023 doi

  16. [24]

    In: PAPM-PROBMIV

    D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and refinement strategies for probabilistic analysis. In: PAPM-PROBMIV. LNCS, vol. 2399, pp. 57–76. Springer (2002). https://doi.org/10.1007/3- 540-45605-8_5

    2002 doi

  17. [25]

    Proceedings of the AAAI Conference on Artificial Intelligence29(1) (Feb 2015)

    Das Gupta, U., Talvitie, E., Bowling, M.: Policy tree: Adaptive representation for policy gradient. Proceedings of the AAAI Conference on Artificial Intelligence29(1) (Feb 2015). https://doi.org/10.1609/aaai.v29i1.9613

    2015 doi

  18. [26]

    Journal of Machine Learning Research23(26), 1–47 (2022), http://jmlr.org/papers/v23/20-520.html

    Demirovi ´c, E., Lukina, A., Hebrard, E., Chan, J., Bailey, J., Leckie, C., Ramamohanarao, K., Stuckey, P.J.: Murtree: Optimal decision trees via dynamic programming and search. Journal of Machine Learning Research23(26), 1–47 (2022), http://jmlr.org/papers/v23/20-520.html

    2022

  19. [27]

    https://doi.org/10.48550/arXiv.1910.03016, https://arxiv.org/abs/ 1910.03016

    Du, S.S., Kakade, S.M., Wang, R., Yang, L.F.: Is a good represen- tation sufficient for sample efficient reinforcement learning? CoRR (2019). https://doi.org/10.48550/arXiv.1910.03016, https://arxiv.org/abs/ 1910.03016

    2019 doi arXiv

  20. [28]

    In: xAI (2)

    Dubslaff, C., Klös, V ., Päßler, J.: Template decision diagrams for meta control and explainability. In: xAI (2). Communications in Computer and Information Science, vol. 2154, pp. 219–242. Springer (2024). https://doi.org/10.1007/978-3-031-63797-1_12

    2024 doi

  21. [29]

    Eisentraut, J., Kelmendi, E., K ˇretínský, J., Weininger, M.: Value iteration for simple stochastic games: Stopping criterion and learning algorithm. Inf. Comput.285(Part), 104886 (2022). https://doi.org/10.1016/j.ic.2022.104886

    2022

  22. [30]

    Esparza, J., K ˇretínský, J., Sickert, S.: A unified translation of linear temporal logic toω-automata. J. ACM67(6), 33:1–33:61 (2020). https://doi.org/10.1145/3417995

    2020 doi

  23. [31]

    In: HICSS

    Gerlings, J., Shollo, A., Constantiou, I.D.: Reviewing the need for ex- plainable artificial intelligence (xAI). In: HICSS. pp. 1–10. ScholarSpace (2021). https://doi.org/10.24251/HICSS.2021.156

    2021 doi

  24. [32]

    Gunning, D., Stefik, M., Choi, J., Miller, T., Stumpf, S., Yang, G.: XAI - explainable artificial intelligence. Sci. Robotics4(37) (2019). https://doi.org/10.1126/scirobotics.aay7120

    2019 doi

  25. [33]

    In: Sankaranarayanan, S., Sharygina, N

    Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner’s guide to MDP model checking algorithms. In: Sankaranarayanan, S., Sharygina, N. (eds.) 29th International Conference on Tools and Algo- rithms for the Construction and Analysis of Systems (TACAS). Lecture...

    2023 doi

  26. [34]

    STTT (to 12 appear), preprint available on github (2026), https://sjunges.github.io/ files/revised_practitioners_guide.pdf

    Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: The revised practitioner’s guide to MDP model checking algorithms. STTT (to 12 appear), preprint available on github (2026), https://sjunges.github.io/ files/revised_practitioners_guide.pdf

    2026

  27. [35]

    In: TACAS (1)

    Hartmanns, A., Klauck, M., Parker, D., Quatmann, T., Ruijters, E.: The quantitative verification benchmark set. In: TACAS (1). Lecture Notes in Computer Science, vol. 11427, pp. 344–350. Springer (2019). https://doi.org/10.1007/978-3-030-17462-0_20

    2019 doi

  28. [36]

    Hensel, C., Junges, S., Katoen, J., Quatmann, T., V olk, M.: The proba- bilistic model checker Storm. Int. J. Softw. Tools Technol. Transf.24(4), 589–610 (2022). https://doi.org/10.1007/S10009-021-00633-Z

    2022 doi

  29. [37]

    Huysmans, J., Dejaeger, K., Mues, C., Vanthienen, J., Baesens, B.: An empirical evaluation of the comprehensibility of decision table, tree and rule based predictive models. Decis. Support Syst.51(1), 141–154 (2011). https://doi.org/10.1016/j.dss.2010.12.003

    2011 doi

  30. [38]

    Hyafil, L., Rivest, R.L.: Constructing optimal binary decision trees is NP-complete. Inf. Process. Lett.5(1), 15–17 (1976). https://doi.org/10.1016/0020-0190(76)90095-8

    1976 doi

  31. [39]

    https://doi.org/10.2759/177365

    Independent High-Level Expert Group on Artificial Intelligence: Ethics guidelines for trustworthy AI - European commission, directorate- general for communications networks, content and technology (2019). https://doi.org/10.2759/177365

    2019 doi

  32. [40]

    In: Proceedings of the ninth annual ACM symposium on Principles of distributed computing

    Israeli, A., Jalfon, M.: Token management schemes and random walks yield self-stabilizing mutual exclusion. In: Proceedings of the ninth annual ACM symposium on Principles of distributed computing. pp. 119–131 (1990)

    1990

  33. [41]

    In: FMCAD

    Jantsch, S., Harder, H., Funke, F., Baier, C.: SWITSS: Computing small witnessing subsystems. In: FMCAD. pp. 236–244. IEEE (2020). https://doi.org/10.34727/2020/ISBN.978-3-85448-042-6_31

    2020 doi

  34. [42]

    In: DASC

    Julian, K., Lopez, J., Brush, J., Owen, M., Kochenderfer, M.: Policy compression for aircraft collision avoidance systems. In: DASC. pp. 1– 10 (09 2016). https://doi.org/10.1109/DASC.2016.7778091

    2016

  35. [43]

    Jüngermann, F., K ˇretínský, J., Weininger, M.: Algebraically explain- able controllers: decision trees and support vector machines join forces. Int. J. Softw. Tools Technol. Transf.25(3), 249–266 (2023). https://doi.org/10.1007/S10009-023-00716-Z

    2023 doi

  36. [44]

    Lecture Notes

    Kallenberg, L.: Markov decision processes. Lecture Notes. University of Leiden428(2011), https://www.researchgate.net/profile/ Lodewijk-Kallenberg/publication/359893791_Lecture_Notes_Markov_ Decision_Processes_-_version_2022/links/62553afbb0cee02d6965cab0/ Lecture-Notes-Markov...

    2011

  37. [45]

    In: 2022 International Conference on Robotics and Automation, ICRA 2022, Philadel- phia, PA, USA, May 23-27, 2022

    Kiesbye, J., Grover, K., Ashok, P., K ˇretínský, J.: Planning via model checking with decision-tree controllers. In: 2022 International Conference on Robotics and Automation, ICRA 2022, Philadel- phia, PA, USA, May 23-27, 2022. pp. 4347–4354. IEEE (2022). https://doi.org/10.11...

    2022

  38. [46]

    In: Workshop on Interpretable Policies in Reinforcement Learning @RLC-2024 (2024), https://openreview.net/forum?id=zafp5CwoTq

    Kohler, H., Delfosse, Q., Akrour, R., Kersting, K., Preux, P.: Inter- pretable and editable programmatic tree policies for reinforcement learn- ing. In: Workshop on Interpretable Policies in Reinforcement Learning @RLC-2024 (2024), https://openreview.net/forum?id=zafp5CwoTq

    2024

  39. [47]

    In: Enea, C., Lal, A

    K ˇretínský, J., Meggendorfer, T., Prokop, M., Rieder, S.: Guessing winning policies in ltl synthesis by semantic learning. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 390–414. Springer Nature Switzerland, Cham (2023)

    2023

  40. [48]

    K ˇretínský, J., Meggendorfer, T.: Of cores: A partial-exploration frame- work for Markov decision processes. Log. Methods Comput. Sci.16(4) (2020). https://doi.org/10.23638/LMCS-16(4:3)2020

    2020 doi

  41. [49]

    In: ATV A

    K ˇretínský, J., Meggendorfer, T., Sickert, S.: Owl: A library forω-words, automata, and LTL. In: ATV A. Lecture Notes in Computer Science, vol. 11138, pp. 543–550. Springer (2018). https://doi.org/10.1007/978-3-030- 01090-4_34

    2018 doi

  42. [50]

    In: CA V (1)

    K ˇretínský, J., Meggendorfer, T., Sickert, S., Ziegler, C.: Rabinizer 4: From LTL to your favourite deterministic automaton. In: CA V (1). Lecture Notes in Computer Science, vol. 10981, pp. 567–577. Springer (2018). https://doi.org/10.1007/978-3-319-96145-3_30

    2018 doi

  43. [51]

    In: CA V

    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verifi- cation of probabilistic real-time systems. In: CA V. Lecture Notes in Computer Science, vol. 6806, pp. 585–591. Springer (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    2011 doi

  44. [52]

    In: 2010 IEEE Globecom Workshops

    Liu, S., Panangadan, A., Talukder, A., Raghavendra, C.S.: Compact rep- resentation of coordinated sampling policies for body sensor networks. In: 2010 IEEE Globecom Workshops. pp. 2044–2048. IEEE (2010). https://doi.org/10.1109/GLOCOMW.2010.5700304

    2010

  45. [53]

    In: Bouajjani, A., Holík, L., Wu, Z

    Meggendorfer, T.: PET - A partial exploration tool for probabilistic verification. In: Bouajjani, A., Holík, L., Wu, Z. (eds.) Automated Tech- nology for Verification and Analysis - 20th International Symposium, ATV A 2022, Virtual Event, October 25-28, 2022, Proceedings. Lect...

    2022 doi

  46. [54]

    In: CA V (3)

    Meggendorfer, T., Weininger, M.: Playing games with your PET: ex- tending the partial exploration tool to stochastic games. In: CA V (3). Lecture Notes in Computer Science, vol. 14683, pp. 359–372. Springer (2024). https://doi.org/10.1007/978-3-031-65633-0_16

    2024 doi

  47. [55]

    Information Systems Management39(1), 53–63 (2022)

    Meske, C., Bunde, E., Schneider, J., Gersch, M.: Explainable arti- ficial intelligence: objectives, stakeholders, and future research op- portunities. Information Systems Management39(1), 53–63 (2022). https://doi.org/10.1080/10580530.2020.1849465

    2022

  48. [56]

    Miller, T., Hoffman, R.R., Amir, O., Holzinger, A.: Special issue on explainable artificial intelligence (XAI). Artif. Intell.307, 103705 (2022). https://doi.org/10.1016/j.artint.2022.103705

    2022

  49. [57]

    McGraw-Hill Series in Computer Science, McGraw-Hill (1997), https://www.worldcat

    Mitchell, T.M.: Machine learning, International Edition. McGraw-Hill Series in Computer Science, McGraw-Hill (1997), https://www.worldcat. org/oclc/61321007

    1997

  50. [58]

    In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems

    Neider, D., Topcu, U.: An automaton learning approach to solving safety games over infinite graphs. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 204–221. Springer (2016)

    2016

  51. [59]

    Phillips, P.J., Hahn, C.A., Fontana, P.C., Broniatowski, D.A., Przy- bocki, M.A.: Four principles of explainable artificial intelligence - (U.S.) national institute of standards and technology (NIST) (2020), https://doi.org/10.6028/NIST.IR.8312-draft

    2020 doi

  52. [60]

    Appl.62, 333–346 (2016)

    Piltaver, R., Lustrek, M., Gams, M., Martincic-Ipsic, S.: What makes classification trees comprehensible? Expert Syst. Appl.62, 333–346 (2016). https://doi.org/10.1016/j.eswa.2016.06.009

    2016 doi

  53. [61]

    In: POPL

    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL. pp. 179–190. ACM Press (1989). https://doi.org/10.1145/75277.75293

    1989

  54. [62]

    In: Proceedings of the third annual ACM symposium on Principles of distributed computing

    Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. In: Proceedings of the third annual ACM symposium on Principles of distributed computing. pp. 12–27 (1984)

    1984

  55. [63]

    Wiley Series in Probability and Statistics, Wiley (1994)

    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dy- namic Programming. Wiley Series in Probability and Statistics, Wiley (1994). https://doi.org/10.1002/9780470316887

    1994 doi

  56. [64]

    Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. Proc. IEEE77(1), 81–98 (1989). https://doi.org/10.1109/5.21072

    1989 doi

  57. [65]

    Rudin, C.: Stop explaining black box machine learning models for high stakes decisions and use interpretable models instead. Nat. Mach. Intell. 1(5), 206–215 (2019). https://doi.org/10.1038/s42256-019-0048-x

    2019 doi

  58. [66]

    CoRR (2016), http://arxiv.org/abs/1511.06295

    Rusu, A.A., Colmenarejo, S.G., Gülçehre, Ç., Desjardins, G., Kirk- patrick, J., Pascanu, R., Mnih, V ., Kavukcuoglu, K., Hadsell, R.: Policy distillation. CoRR (2016), http://arxiv.org/abs/1511.06295

    2016 arXiv

  59. [67]

    Bell Syst

    Shannon, C.E.: A mathematical theory of communication. Bell Syst. Tech. J.27(4), 623–656 (1948). https://doi.org/10.1002/j.1538- 7305.1948.tb00917.x

    1948

  60. [68]

    IEEE Trans

    Tjoa, E., Guan, C.: A survey on explainable artificial intelligence (XAI): Toward medical XAI. IEEE Trans. Neural Networks Learn. Syst.32(11), 4793–4813 (2021). https://doi.org/10.1109/TNNLS.2020.3027314

    2021

  61. [69]

    In: AAAI

    Topin, N., Milani, S., Fang, F., Veloso, M.: Iterative bounding MDPs: Learning interpretable policies via non-interpretable methods. In: AAAI. pp. 9923–9931. AAAI Press (2021). https://doi.org/10.1609/AAAI.V35I11.17192

    2021 doi

  62. [70]

    In: Dy, J., Krause, A

    Verma, A., Murali, V ., Singh, R., Kohli, P., Chaudhuri, S.: Programmat- ically interpretable reinforcement learning. In: Dy, J., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol. 80, pp. 5045...

    2018

  63. [71]

    waiting for a request

    V os, D., Verwer, S.: Optimal decision tree policies for Markov decision processes. In: IJCAI. pp. 5457–5465. ijcai.org (2023). https://doi.org/10.24963/IJCAI.2023/606 13 APPENDIX A. Linear Temporal Logic and Decision Trees We extend our approach to also represent (ε-optimal) ...

    2023 doi

  64. [73]

    •dtNESt: We tried using the artefact at DOI 10.5281/ zenodo.15642001

    Details on Tool Configurations:For the competitors in our experimental evaluation, we used the following configura- tions: •dtControl 2: We use the default con- figuration ofdtControl 2, using commit 6e0eb73c2d67a77611ad015c4fea9f7917c83da1 of our extension (https://gitlab.com...

  65. [74]

    We start by comparing the different datasets in Tables IV to VI and find that, depending on the model, the impact of the heuristics varies widely

    Summary of Additional Results:The following sections provide deeper insights and more data about our experiments. We start by comparing the different datasets in Tables IV to VI and find that, depending on the model, the impact of the heuristics varies widely. Applying the com...

  66. [75]

    Results are shown in Table IV forPermissive, Table V forCombined, and Table VI andController

    Sizes for Dataset Construction:We compare the number of states that can be reduced by the different relevance heuris- tics across the different dataset configurations. Results are shown in Table IV forPermissive, Table V forCombined, and Table VI andController. Mostly, we foun...

  67. [76]

    We highlight the columns fordtPaynt

    Results on DT Sizes:Table VII shows the sizes of the computed DTs. We highlight the columns fordtPaynt. While the tool aims to provide the smallest possible DTs, we found provably smaller ones, suggesting either an internal timeout during some steps of the computation or a bug...

  68. [77]

    Results on Runtime:This section compares run- time across the different configurations implemented in dtControl 2 +ε, as well as withdtNESt

  69. [78]

    We also exclude the time for pruning, as pruning often tends to exhaust the given budget

    Comparison of Different Configurations:For the follow- ing experiments, we measured the time withindtControl 2 and excluded the time required for model solving, as it is the same for all methods. We also exclude the time for pruning, as pruning often tends to exhaust the given...

  70. [79]

    For both, we measured the time outside of the Docker container, meaning the time includes startup and shut- down

    Runtime Comparison todtNESt:In this section, we report on the runtime of thedtControl 2 +εportfolio and dtNESt. For both, we measured the time outside of the Docker container, meaning the time includes startup and shut- down. Experiments were repeated 5 times.dtControl 2 +ε is...

    2020

  71. [381]

    https://doi.org/10.24963/ijcai.2023/42

    ijcai.org (2023). https://doi.org/10.24963/ijcai.2023/42

    2023 doi

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.