Pith. sign in

REVIEW 2 major objections 4 minor 43 references

Small Decision Trees for MDPs with Deductive Synthesis

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

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

Pith's one-line read This paper establishes that the bounded-depth decision-tree synthesis problem for MDPs can be solved by a sound and complete abstraction-refinement loop, and that an SMT-based implementation scales beyond the previous MILP-based tool…

desk verdict A real, reproducible systems contribution for synthesizing small decision-tree MDP policies; the main loop is sound, but the NP-hardness proof is faulty and the fallback semantics deserves more careful framing. read the letter →

arxiv 2501.10126 v2 pith:VD2M564G submitted 2025-01-17 cs.LO

Roman Andriushchenko , Milan Češka , Sebastian Junges , Filip Macák This is my paper · ORCID
classification cs.LO MSC 68Q6090C4068Q17
keywords Markovdecisionprocessestreepoliciesbounded-depthsynthesisabstractionrefinementSMTsolvingpolicycompressionunsatisfiablecoresmodelchecking
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

Optimal policies of Markov decision processes are usually lookup tables, too large for a human to inspect, so a natural goal is to compress them into small decision trees. This paper targets the harder variant: instead of compressing one fixed optimal policy, search directly over all policies induced by decision trees of depth at most $k$ and return the tree with the best reachability, reward, or discounted value. The proposed loop, dtPaynt, alternates model checking of an overapproximating family of MDPs with SMT queries that decide whether an abstract optimal policy can be realized by a tree; when it cannot, an unsatisfiable core and a harmonizing pair of parameterizations guide a split. The authors prove the loop sound and complete, and their experiments show it outperforms the prior MILP-based solver on larger models and, with a heuristic mapping tool, cuts tree sizes by up to 90% while sacrificing under 1% of value on a 1.5-million-state model.

What carries the argument

The load-bearing object is the tree template with parameterizations: a template is a binary tree whose nodes are not yet assigned predicates or actions, and a parameterization $f=(D,B,A)$ chooses a variable index, a bound, and an action for each node, thereby instantiating a concrete decision tree. The abstraction-refinement engine then uses the family-MDP $M(\mathcal{F})$, defined so that an action is available in a state exactly when some parameterization in $F$ could produce it, giving a sound upper bound on the value of every tree in the family. When the optimal policy of $M(\mathcal{F})$ is spurious, the SMT encoding of the mapping problem returns an unsatisfiable core together with harmonizing parameterizations $f_1,f_2$ that differ in exactly one variable; splitting the domain of that harmonizing variable bisects the family in a way informed by the conflict, and the loop repeats until every family is pruned or realized.

What would settle it

Take a small benchmark such as lake-4, fix $k=2$, exhaustively enumerate every depth-2 decision tree over the allowed predicates, and compare the maximum value of that enumeration with dtPaynt's output; any gap would refute Theorem 4. A cheaper conceptual check is to modify the fallback rule so leaves may only name available actions; if the best value drops, the paper's optimality claim is tied to the randomized-fallback semantics rather than to fully realizable deterministic trees.

Watch

Extended reading notes

Core claim

The central discovery is that the bounded-depth synthesis problem — maximize the value over all policies representable by a decision tree of depth at most $k$ — reduces to a finite search over rectangular families of tree parameterizations, with each family overapproximated by a sub-MDP. For a family $F$ of parameterizations, the family-MDP $M(\mathcal{F})$ enables an action exactly in states where some assignment in $F$ could select it, so its optimal policy $\sigma$ has value at least that of any tree in $F$. If $\sigma$ itself is $F$-implementable, the SMT encoding returns a witness and the search for that family is done; if not, an unsatisfiable core isolates a small set of critical states, and two harmonizing parameterizations differing in a single variable show where the family must be split. Because every split shrinks a finite domain and each leaf is a single parameterization with a single policy, the loop always terminates and never discards an optimal assignment, which is the content of Theorem 4. On large benchmarks this makes the anytime version of the problem practical: good trees are found early via bounded-depth iteration and tree hints, and the same machinery can repair subtrees of a large tree compositionally.

Load-bearing premise

The whole optimality result depends on the convention that a leaf action unavailable at a state is replaced by the uniform random action, so the class of $k$-implementable policies contains randomized fallback behavior rather than only deterministic policies whose leaf actions are always available.

Editorial extensions

If this is right

  • For any MDP and depth bound $k$ for which a good $k$-implementable policy exists, the algorithm will eventually return the best one instead of settling for a compression of a precomputed table.
  • The optimality guarantee must be read with the random-fallback semantics: a leaf naming an action unavailable in a state plays $\alpha_{\mathrm{rand}}$, and this is why a depth-0 tree can already be optimal for models like ij-20.
  • On the tested models with up to 10k states, the SMT-based approach outperforms the monolithic MILP approach, and the advantage grows with depth because the abstraction-refinement loop prunes rather than enumerates.
  • When paired with a heuristic policy-to-tree mapper, the same machinery reduces large trees, for example from 236 to 22 inner nodes on a 1.5M-state model, while losing less than 1% of optimal value.

Reading between the lines

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

  • The random-action fallback means the headline size reductions compare policies that may randomize when a leaf action is unavailable against exact policy trees; a reader wanting purely deterministic, always-available leaf actions is looking at a different, harder optimization target than the one Theorem 4 certifies.
  • The template-and-harmonization recipe is not specific to depth-bounded trees: any policy class that admits a finite parameterization and a harmonizing split could in principle be synthesized by the same abstraction-refinement scheme.
  • Because the algorithm's baseline is the uniform-random 0-tree, its normalized-value reports could be used to pick the smallest depth that meets a performance budget, turning depth selection into a simple online stopping rule.
Share X Bluesky LinkedIn Reddit HN

Formalized claims in Lean

  1. Claim #1: The central discovery is that the bounded-depth synthesis problem — maximize the value over all policies representable by a decision tree of depth at most $k$ — reduces to a finite search over rectangular families of tree parameterizations, with each family overapproximated by a sub-MDP. For a family $F$ of parameterizations, the family-MDP $M(\mathcal{F})$ enables an action exactly in states wher

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 studies the synthesis of small decision-tree (DT) policies for Markov decision processes. It introduces an SMT-based encoding of a fixed tree template (Section 3.1), including unsatisfiable-core-based diagnosis and a harmonization technique (Section 3.2), and combines these with an abstraction-refinement loop (Algorithm 1) to find a DT of bounded depth with maximum reachability/reward value. The central formal result is Theorem 4, which states that Algorithm 1 is sound and complete for this objective under the induced-policy semantics of Definition 4. The experimental section compares dtPaynt with OMDT and dtControl, reporting scalability to hundreds of thousands of states and size reductions up to 90% on a 1.5M-state model at 1% value loss.

Significance. If the results hold, the paper makes a useful contribution to the concise-policy-synthesis literature: it offers a deductive, SMT-driven alternative to monolithic MILP encodings, with public code and benchmarks. The abstraction-refinement loop with harmonizing parameterizations is a clever adaptation of prior Paynt ideas. The main caveats are that the random-action fallback in Definition 4 changes the policy class in some of the experiments, weakening the explanatory-power interpretation, and that the NP-hardness proof in Appendix A.4 is, as written, not a valid reduction. Neither issue invalidates the core synthesis algorithm, but both need to be addressed before the empirical and complexity-theoretic claims can be taken at face value.

major comments (2)
  1. [§4.2 / §5, Q3 and Q4; Definition 4; Remark 2] The fallback semantics of Definition 4 — a leaf prescribing an unavailable action induces the random action αrand — is explicit and coherent, and Theorem 4 is sound for it. However, the paper's interpretability claims and some empirical comparisons are affected. In Q3 (Table 1), the 0-DT for ij-20 is optimal precisely because the fallback lets the single leaf action be replaced by αrand where the action is unavailable, and the Q4 reduction of the csma-Q4 DT (90% size reduction) can likewise rely on fallback leaves. dtControl, by contrast, is run on a fixed tabular policy and does not have this fallback freedom, so the reported size advantages in these experiments compare policies in different classes. Moreover, a tree whose displayed leaf action is not actually executed is a weaker fit for the stated motivation of human-readable policies. Please rerun the Q3/Q4 experiments with the fallback disabled (leaf actions restricted to Act(s)) or, if fallback is retained, report how often it is actually used, and provide a dtControl baseline that is given the same fallback capability.
  2. [Appendix A.4, Theorem 3] The NP-hardness reduction from X3C is not correct as written. The state variables include a variable for every state s with s(v)=1 only in that state; since predicates are of the form v≤b, the predicate 'v≤0' uniquely identifies that state. With these predicates a tree of depth about log2(|S|) can distinguish all n+3 states without using any set predicates from T, and for n>7 this depth is strictly smaller than k=|U|/3+2. Hence the claimed equivalence with the existence of an exact cover fails even when no exact cover exists. The combinatorial step in the 'Correctness' paragraph is asserted without proof, and the citation to [28] is to the PRISM 4.0 paper, which does not support the claim. The theorem may be true, but the proof must be repaired or the claim removed.
minor comments (4)
  1. [Appendix A.4] The reference '[28]' in the correctness argument should be replaced by the intended source; as written it points to the PRISM 4.0 tool paper.
  2. [Section 5, Setting] The modification that makes every action available in every state is disclosed, but the paper should state explicitly that the baseline tools and dtPaynt are all evaluated on this modified MDP, and should comment on how the fallback αrand interacts with this modification.
  3. [Theorem 2 statement] The word 'impelementable' is misspelled; it should be 'implementable'.
  4. [Section 4.2, paragraph after Algorithm 1] The termination argument states that any nontrivial splitting makes Algorithm 1 terminate; since this rests on splitInformed and splitArbitrary always producing strictly smaller parameter families, it would be clearer to state and prove this property explicitly.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the SMT encoding and abstraction-refinement soundness proof are self-contained, and self-citations are not load-bearing.

full rationale

The paper's central derivation chain is self-contained rather than circular. Theorem 4, the soundness and completeness of Algorithm 1, is proved in Appendix A.5 directly from the definition of the family-MDP abstraction (Definition 11) and Proposition 2, which states that every tree-induced policy is contained in the abstract family-MDP. The pruning argument uses only V(sigma) >= max_{f in F} V(f), so the algorithm does not presuppose the optimal tree it claims to find. Theorem 1, the correctness of the SMT encoding, is likewise proved from Definitions 4 and 7 without importing the target result. The abstraction-refinement loop is said to be 'borrowed from [13]', and the harmonization idea is connected to the authors' earlier POMDP work [2], but these self-citations are used as heuristic inspiration and are not load-bearing: the termination and optimality arguments are proved in the paper. The experimental claims are benchmarked against external tools OMDT and dtControl on standard models, and no fitted parameter is later renamed as a prediction. The random-action fallback of Definition 4 does mean that the trees synthesized by dtPaynt induce policies in a different class than the exact policy trees produced by dtControl, and the NP-hardness proof in Appendix A.4 appears to have a correctness gap because per-state predicate variables may allow all n+3 states to be distinguished without using set predicates; however, these are correctness and interpretability concerns, not instances of a derivation reducing to its own inputs. No circular step satisfying the quoted-evidence standard was found.

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

The paper's central result depends on standard MDP theorems and tool correctness; no fitted physical constants are used. The only hand-tuned value is the time allocation in the bounded-depth mode, which is an engineering choice rather than a scientific parameter.

free parameters (1)
  • bounded-depth time allocation ratio = lower depths get t/(2*kmax), deepest depth gets the remaining half
    Chosen empirically in Sec. 4.2 to balance the anytime search; affects results under the 20-minute timeout but not the correctness of Algorithm 1.
assumptions (3)
  • standard math For reachability and expected reward objectives, an optimal memoryless deterministic policy exists.
    Invoked in Sec. 2.1 and App. A.1 via Puterman [34, Thm 7.9.1]; unproved in this paper, standard in MDP theory.
  • domain assumption The MDP is finite-state with bounded integer variables in PRISM style.
    Sec. 2.1 restricts to this setting; the parameterization and finite bound set F_T depend on finiteness of states and variable values.
  • domain assumption The SMT solver Z3 and the model checker Storm are correct and implement the claimed theories.
    Used in the SMT encoding (Sec. 3) and for model checking the family MDPs (Alg. 1, line 5); correctness is assumed as standard tooling.
invented entities (1)
  • random action αrand
    purpose: Fallback action for states where a DT leaf selects an unavailable action; enables smaller trees and simplifies availability handling.
    Introduced in Sec. 2.1 and Remark 2. It is a mathematical construction, not an empirical entity, and its soundness is argued via Corollary 1 rather than external evidence.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Small Decision Trees for MDPs with Deductive Synthesis." pith.science (2026). https://pith.science/paper/VD2M564G

@misc{pith2026250110126,
  author       = {Pith},
  title        = {Pith review of: Small Decision Trees for MDPs with Deductive Synthesis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VD2M564G}},
  note         = {Machine review of arXiv:2501.10126}
}
read the original abstract

Markov decision processes (MDPs) describe sequential decision-making processes; MDP policies return for every state in that process an advised action. Classical algorithms can efficiently compute policies that are optimal with respect to, e.g., reachability probabilities. However, these policies are then given in a tabular format. A longstanding challenge is to represent optimal or almost-optimal policies concisely, e.g., as decision trees. This paper makes two contributions towards this challenge: first, an SMT-based approach to encode a given (optimal) policy as a small decision tree, and second, an abstraction-refinement loop that searches for policies that are optimal within the set of policies that can be represented with a small tree. Technically, the latter combines the SMT encoding with verification approaches for families of Markov chains. The empirical evaluation demonstrates the feasibility of these approaches and shows how they can outperform the state-of-the-art on various benchmarks, yielding up to 20 times smaller trees representing (almost) optimal policies for models with up to 10k states and 19 variables.

Figures

Figures reproduced from arXiv: 2501.10126 by the authors.

Figure 1
Figure 1. (a) A simple slippery maze. The goal is to lead the robot placed in the [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. MDP construction for the reduction from X3C problem. [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. Comparison on the bounded-depth synthesis problem for Q1. The scatter [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: The plot shows the trade-off between the value and size of the DTs found [PITH_FULL_IMAGE:figures/full_fig_p017_4.png]
Figure 5
Figure 5. Figure 5: (a) The Exact Cover by 3-sets (X3C) problem formulation. (b) MDP [PITH_FULL_IMAGE:figures/full_fig_p026_5.png]
Figure 6
Figure 6. Figure 6: Comparison in runtimes between dtPaynt and OMDT. Only experiments where the normalized values of the trees found by the tools are within 10% of each other. the resulting table as a CSV file available here: https://anonymous.4open. science/r/dt-synthesis-cav-25-5B31/res…
Figure 7
Figure 7. Figure 7: Complete graph for Q2, including all models from our benchmark set. [PITH_FULL_IMAGE:figures/full_fig_p029_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 39 canonical work pages

  1. [28]

    In: CA V

    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CA V. LNCS, vol. 6806, pp. 585–591. Springer (2011)

    work page 2011

  2. [1]

    In: TACAS

    Andriushchenko, R., ˇCeˇ ska, M., Junges, S., Katoen, J.P.: Inductive synthesis for probabilistic programs reaches new horizons. In: TACAS. LNCS, vol. 12651, pp. 191–209. Springer (2021)

    work page 2021

  3. [2]

    Andriushchenko, R., ˇCeˇ ska, M., Junges, S., Katoen, J.P.: Inductive synthesis of finite-state controllers for POMDPs. In: UAI. vol. 180, pp. 85–95. PMRL (2022)

    work page 2022

  4. [3]

    In: CA V

    Andriushchenko, R., ˇCeˇ ska, M., Junges, S., Katoen, J.P., Stupinsk´ y,ˇS.: PAYNT: a tool for inductive synthesis of probabilistic programs. In: CA V. LNCS, vol. 12759, pp. 856–869. Springer (2021)

    work page 2021

  5. [4]

    In: UAI (to appear) (2025)

    Andriushchenko, R., ˇCeˇ ska, M., Chakraborty, D., Junges, S., Kˇ retinsk´ y, J., Mac´ ak, F.: Symbiotic local search for small decision tree policies in MDPs. In: UAI (to appear) (2025)

    work page 2025

  6. [5]

    In: TACAS

    Ashok, P., Jackermeier, M., Kˇ ret ´ ınsk` y, J., Weinhuber, C., Weininger, M., Yadav, M.: dtcontrol 2.0: Explainable strategy representation via decision tree learning steered by experts. In: TACAS. LNCS, vol. 12652, pp. 326–345. Springer (2021)

    work page 2021

  7. [6]

    In: QEST

    Ashok, P., Kˇ ret ´ ınsk` y, J., Larsen, K.G., Le Co¨ ent, A., Taankvist, J.H., Weininger, M.: SOS: safe, optimal and small strategies for hybrid Markov decision processes. In: QEST. pp. 147–164. Springer (2019)

    work page 2019

  8. [7]

    In: Handbook of Model Checking, pp

    Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking, pp. 963–999. Springer (2018)

    work page 2018

Show all 43 references
  1. [8]

    Advances in neural information processing systems 31 (2018)

    Bastani, O., Pu, Y., Solar-Lezama, A.: Verifiable reinforcement learning via policy extraction. Advances in neural information processing systems 31 (2018)

    2018

  2. [9]

    Proceedings of the ACM on Programming Languages 8(POPL), 2792–2820 (2024)

    Batz, K., Biskup, T.J., Katoen, J.P., Winkler, T.: Programmatic strategy synthesis: Resolving nondeterminism in probabilistic programs. Proceedings of the ACM on Programming Languages 8(POPL), 2792–2820 (2024)

    2024

  3. [10]

    Biere, A., Heule, M., van Maaren, H.: Handbook of satisfiability, vol. 185. IOS press (2009)

    2009

  4. [11]

    In: CA V

    Br´ azdil, T., Chatterjee, K., Chmel ´ ık, M., Fellner, A., Kˇ ret ´ ınsk` y, J.: Counterexample explanation by learning small strategies in Markov decision processes. In: CA V. pp. 158–177. Springer (2015)

    2015

  5. [12]

    In: ISoLA

    Budde, C.E., Hartmanns, A., Klauck, M., Kˇ ret ´ ınsk´ y, J., Parker, D., Quatmann, T., Turrini, A., Zhang, Z.: On correctness, precision, and performance in quantitative verification: QComp 2020 competition report. In: ISoLA. pp. 216–241. Springer (2020)

    2020

  6. [13]

    In: TACAS

    ˇCeˇ ska, M., Jansen, N., Junges, S., Katoen, J.P.: Shepherding hordes of Markov chains. In: TACAS. LNCS, vol. 11428, pp. 172–190. Springer (2019)

    2019

  7. [14]

    In: ICAPS

    Chatterjee, K., Chmelik, M., Topcu, U.: Sensor synthesis for pomdps with reacha- bility objectives. In: ICAPS. pp. 47–55. AAAI Press (2018)

    2018

  8. [15]

    In: TACAS

    David, A., Jensen, P.G., Larsen, K.G., Mikuˇ cionis, M., Taankvist, J.H.: Uppaal stratego. In: TACAS. pp. 206–211. Springer (2015)

    2015

  9. [16]

    In: ATV A

    Dehnert, C., Jansen, N., Wimmer, R., ´Abrah´ am, E., Katoen, J.P.: Fast debugging of PRISM models. In: ATV A. LNCS, vol. 8837, pp. 146–162. Springer (2014)

    2014

  10. [17]

    In: TACAS

    Delgrange, F., Katoen, J.P., Quatmann, T., Randour, M.: Simple strategies in multi-objective mdps. In: TACAS. pp. 346–364. Springer (2020)

    2020

  11. [18]

    Logical Methods in Computer Science 11 (2015)

    Drager, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. Logical Methods in Computer Science 11 (2015)

    2015

  12. [19]

    Dubslaff, C., Kl¨ os, V., P¨ aßler, J.: Template decision diagrams for meta control and explainability. In: XAI. pp. 219–242. Springer (2024) 22 Andriushchenko et al

    2024

  13. [20]

    In: AAAI

    Gupta, U.D., Talvitie, E., Bowling, M.: Policy tree: Adaptive representation for policy gradient. In: AAAI. vol. 29 (2015)

    2015

  14. [21]

    Information and Computation 126(2), 114–122 (1996)

    Hancock, T., Jiang, T., Li, M., Tromp, J.: Lower bounds on learning decision lists and trees. Information and Computation 126(2), 114–122 (1996)

    1996

  15. [22]

    In: AAAI/IAAI

    Hauskrecht, M.: Incremental methods for computing bounds in partially observable Markov decision processes. In: AAAI/IAAI. pp. 734–739 (1997)

    1997

  16. [23]

    Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589–610 (2022)

    2022

  17. [24]

    In: TACAS

    Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.: Safety-constrained reinforcement learning for MDPs. In: TACAS. LNCS, vol. 9636, pp. 130–146. Springer (2016)

    2016

  18. [25]

    Preprint arXiv:2405.14956 (2024)

    Kohler, H., Delfosse, Q., Akrour, R., Kersting, K., Preux, P.: Interpretable and editable programmatic tree policies for reinforcement learning. Preprint arXiv:2405.14956 (2024)

    2024 arXiv

  19. [26]

    Konsta, A.M., Lluch Lafuente, A., Matheja, C.: What should be observed for optimal reward in pomdps? In: CA V. pp. 373–394. Springer (2024)

    2024

  20. [27]

    In: ICAPS

    Kumar, A., Zilberstein, S.: History-based controller design and optimization for partially observable MDPs. In: ICAPS. pp. 156–164. AAAI Press (2015)

    2015

  21. [29]

    Information processing letters 5(1), 15–17 (1976)

    Laurent, H., Rivest, R.L.: Constructing optimal binary decision trees is np-complete. Information processing letters 5(1), 15–17 (1976)

    1976

  22. [30]

    European Journal of Operational Research 211(3), 556–567 (2011)

    Li, Y., Yin, B., Xi, H.: Finding optimal memoryless policies of pomdps under the expected average reward criterion. European Journal of Operational Research 211(3), 556–567 (2011)

    2011

  23. [31]

    Robotics and Autonomous Systems 131, 103568 (2020)

    Likmeta, A., Metelli, A.M., Tirinzoni, A., Giol, R., Restelli, M., Romano, D.: Combining reinforcement learning with rule-based controllers for transparent and general decision-making in autonomous driving. Robotics and Autonomous Systems 131, 103568 (2020)

    2020

  24. [32]

    In: TACAS

    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS. pp. 337–340. Springer (2008)

    2008

  25. [33]

    In: IJCAI

    Narodytska, N., Ignatiev, A., Pereira, F., Marques-Silva, J.: Learning optimal decision trees with SAT. In: IJCAI. pp. 1362–1368. AAAI Press (2018)

    2018

  26. [34]

    Wiley Series in Probability and Statistics, Wiley (1994)

    Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Pro- gramming. Wiley Series in Probability and Statistics, Wiley (1994)

    1994

  27. [35]

    John Wiley & Sons (2014)

    Puterman, M.L.: Markov decision processes: discrete stochastic dynamic program- ming. John Wiley & Sons (2014)

    2014

  28. [36]

    MIT Press (2018)

    Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press (2018)

    2018

  29. [37]

    In: AAAI

    Topin, N., Milani, S., Fang, F., Veloso, M.: Iterative bounding mdps: Learning interpretable policies via non-interpretable methods. In: AAAI. vol. 35, pp. 9923– 9931 (2021)

    2021

  30. [38]

    ˇCeˇ ska, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-guided inductive synthesis for probabilistic systems. Form. Asp. Comput. 33(4–5), 637–667 (2021)

    2021

  31. [39]

    In: ICML

    Verma, A., Murali, V., Singh, R., Kohli, P., Chaudhuri, S.: Programmatically interpretable reinforcement learning. In: ICML. vol. 80, pp. 5052–5061. PMLR (2018)

    2018

  32. [40]

    In: IJCAI

    Vos, D., Verwer, S.: Optimal decision tree policies for Markov decision processes. In: IJCAI. pp. 5457–5465 (2023) Small Decision Trees for MDPs with Deductive Synthesis 23 A Proofs In the following, assume an MDP M = ( S, s0, Act, P) and a tree template T = (T, Γ, ∆). Lemma 1...

    2023

  33. [41]

    V (M ′) ≥ V (M ) - this follows directly from the construction of M ′ since its action space is a superset of M

  34. [42]

    V (M ′) ≤ V (M ) - if there exists a schedulerσ′ in M ′ such that V (σ′) > V(M ), then σ′ can be transformed into a randomized scheduler σrand for the original MDP M with the same value. This transformation simply changes all the de- cisions of the scheduler that chose the new...

  35. [43]

    the decision tree that achieves value above 0 .5 indeed needs to distinguish all these n+3 states into separate leaf nodes

    i.e. the decision tree that achieves value above 0 .5 indeed needs to distinguish all these n+3 states into separate leaf nodes. Definition of state variables. The MDP will have state variables set V = T ∪ S, and the state mapping s : V → Z such that ∀Ti ∈ T : s(Ti) = 1 if s ∈...

    1950

Pith tools

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