Pith. sign in

REVIEW 3 major objections 5 minor 52 references

Grouping factored MDP states by shared causal reasons for a property yields small abstractions that still support near-optimal policies.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · grok-4.5

2026-07-30 21:07 UTC pith:2TKJOP4P

load-bearing objection Solid foundational pipeline for property-driven causal MDP abstraction; the full-solve prerequisite is openly admitted and caps practical impact, but does not erase the formal or empirical contribution. the 3 major comments →

arxiv 2607.26787 v1 pith:2TKJOP4P submitted 2026-07-29 cs.AI cs.LO

Property-driven Causal Abstractions for Markov Decision Processes

Jule Schmidt , Maximilian Weininger , Clemens Dubslaff , David Parker , Nils Jansen This is my paper
classification cs.AI cs.LO
keywords Markov decision processescausal abstractionfeature causalitypredicate abstractioninterval MDPsstochastic gamesfactored MDPspolicy transfer
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Factored MDPs explode in size as state variables grow, yet many states share the same reasons a reachability or safety property holds or fails. This paper treats variable valuations as Boolean features, finds minimal feature sets that cause property satisfaction or violation, and partitions states that share those causes. The partitions are turned into smaller abstract models by averaging transitions, wrapping them in probability intervals, or letting an opponent pick a concrete representative inside each group. On standard benchmarks the resulting models are often a small fraction of the original size, and policies solved on them transfer back with near-optimal performance. Causes computed on small parameter settings frequently still produce useful abstractions of related large-scale models.

Core claim

Property-driven feature causality on factored MDPs produces state-space partitions that, when aggregated into ordinary MDPs, interval MDPs, or stochastic games, retain enough structure that near-optimal policies for the original model can be recovered from the abstraction, and the same causes often generalize from small model variants to related large ones.

What carries the argument

Feature causes—minimal assignments over state-variable predicates sufficient for an effect set defined by value thresholds on the property—used to build one-shot, iterative, or causal-graph partitions, then aggregated by weighted average, interval bounds, or opponent choice in a stochastic game.

Load-bearing premise

The method currently requires an exact full analysis of the original MDP, and sometimes several reachability queries, just to discover the causes that will shrink it.

What would settle it

If, on the reported PRISM/Storm benchmarks, policies transferred from causal SG or IMDP abstractions consistently showed large normalized policy differences even under “good” effect sets and iterative partitions, or if causes from small models systematically failed to reduce large related models while preserving any policy quality, the central empirical claim would be false.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Small causal abstractions can replace full MDP solving for near-optimal policy extraction on several standard models.
  • Causes computed on tiny parameter settings can be reused as partitions for much larger related MDPs without recomputing causality.
  • Stochastic-game aggregation gives tighter value bounds and better transferred policies than interval or average aggregation.
  • Effect sets focused on states near property satisfaction produce better partitions than those focused on violation.
  • Iterative causal partitions outperform one-shot and causal-graph partitions on policy quality at higher computational cost.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If effect sets and causes can later be approximated from samples or from small solved instances, the same partition-and-aggregate pipeline could become a practical preprocessor for model checking and RL without ever solving the large MDP exactly.
  • The edge of SG aggregation over intervals and averages suggests that preserving adversarial choice among concrete representatives carries more decision-relevant information than summary statistics alone.
  • The method depends on factored variables that carry structural meaning; unstructured or highly synthetic state spaces where every variable is locally critical are unlikely to shrink usefully.
  • Multi-objective or constrained MDPs could use the same machinery by defining effect sets from several value functions at once.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper introduces feature causality for factored MDPs and a property-driven abstraction pipeline: effect/Valid sets are formed from reachability (or safety) values via thresholds, minimal causes over state-variable predicates are extracted, states are partitioned (one-shot PredPart/C-1, iterative C-IT, or causal-graph C-G), and partitions are aggregated into weighted-average MDPs, IMDPs, or stochastic games. Theorem 1 relates C-G and PredPart coarseness; Theorem 2 establishes that WA gives no value guarantees while IMDP/SG sandwich the original values (with appendix proofs). Experiments on PRISM/Storm benchmarks compare partitions and aggregations (RQ1–RQ3) and test small-to-large cause transfer (RQ4), reporting substantial size reduction and, on several models, near-optimal transferred policies, while openly noting that full-model analysis is currently required to obtain causes.

Significance. If the framework holds, it supplies a clean formal bridge from feature causality to state abstraction in factored MDPs, with three aggregation semantics and explicit value-bound theorems. Strengths include appendix proofs for Theorems 1–2 (standard VI/consistency arguments; SG bounds reuse Kattenbelt et al.), a reproducible implementation on Storm/PRISM with public code, and an unusually candid limitations discussion. The empirical picture is mixed but informative: C-IT-SG is most reliable, C-G often leaves the model unchanged, and causes can shrink large instances. The work is a solid foundational step for causal abstraction in formal verification and RL, even if practical scalability is deferred to approximation/transfer.

major comments (3)
  1. [Abstract; §I; §IV-B,C; §VII] Abstract, §I (Results/Limitations), and §VII claim that causal abstractions mitigate state-space explosion and yield small models supporting near-optimal original policies. Realizing any of C-1, C-IT, or C-G requires exact value analysis of the full concrete MDP to build Effect/Valid sets (§IV-B,C; Fig. 4), often plus multiple reachability queries for C-IT—precisely the analysis abstractions are meant to avoid. The only offered escape is small-to-large transfer (RQ4). This is acknowledged as future work, but the central scalability claim in the abstract and introduction is therefore stronger than what the present pipeline demonstrates and should be restated to match the foundational scope.
  2. [RQ4; Fig. 9; Abstract; §I] RQ4 and Fig. 9 report that causes from small models reliably shrink relative size of medium/large instances (<20%), yet “the policy difference often becomes worse, sometimes degrading to the worst possible policy.” The abstract’s phrasing that abstractions “often generalize to related large-scale MDP models” and the §I claim of near-optimal policies therefore overstate the quality half of transfer. The paper should quantify failure rates (e.g., fraction of benchmarks with policy difference near 0 vs near 1) and qualify the generalization claim accordingly, or restrict it to size only.
  3. [§VI RQ1; Appendix C-A; Table I] §VI and Appendix C show strong sensitivity to Effect/Valid semantics (“good” vs “bad” bands), threshold type (relative ε=0.1 preferred), and iteration count k for C-IT, with hyperparameters fixed after a small-model sweep. Free parameters (ε, k, Effect configuration) are load-bearing for the reported “best” C-IT-SG results. A clearer protocol—e.g., default settings justified a priori, or a small sensitivity table on held-out models—would make the empirical claims more robust and reproducible without re-tuning per benchmark family.
minor comments (5)
  1. [Fig. 3; Fig. 6; Appendix C] Fig. 3 and Fig. 6 are helpful but the taxi partition colors and the SG agent/opponent distinction would benefit from a short legend in the caption; several appendix figures (11–19) are referenced densely and hard to parse without higher resolution or clearer axis labels.
  2. [§IV-A; Example 5] Notation for ordinal predicates (X_i ≥ x_{i,k}) vs categorical (X_i = x_{i,k}) is clear in §IV-A, but the simplification “write X_i instead of X_i ≥ 1” for binary variables is easy to miss; a one-line reminder when battery/passenger appear in examples would help.
  3. [§II] Related work (§II) covers causal RL and bisimulation well; a brief pointer to how PredPart differs from standard predicate abstraction refinement loops (beyond the one sentence in the introduction) would situate the contribution more sharply for the FMCAD audience.
  4. [Table II; Remark 3] Table II lists benchmarks cleanly; stating explicitly which properties are reach-avoid vs pure reachability in the main text (currently only in Remark 3) would avoid confusion when reading RQ1–RQ3.
  5. [§IV-C; §II; §III-B] Minor typos: “fixate on states” (§IV-C), “Sim ˜ao” spacing, and occasional missing spaces before citations; “opt := min if opt = max” is standard but the dual notation opt/¯opt could be introduced once in a display.

Circularity Check

0 steps flagged

No derivation-chain circularity: causes, partitions, and abstractions are independently defined and evaluated against external MDP ground truth.

full rationale

The paper’s pipeline is Effect/Valid sets from exact reachability values V(s) → feature causes (Def. 4, adapted from prior feature-causality work) → PredPart / IterPredPart / CGPart → WA/IMDP/SG aggregation → comparison of abstract size, value bounds, and transferred-policy quality against the original MDP’s optimal value. None of these steps reduces by construction to its own input: causes are minimal sufficient predicate assignments for independently thresholded effect sets (Fig. 4; §IV-B,C); aggregation definitions (Defs. 5–7) and value-bound theorems (Thm. 2) are standard and proved with counter-examples and induction, not fitted; empirical metrics (relative size, interval width, normalized policy difference) are measured on the concrete MDP. Citation of the authors’ feature-causality line [8] supplies a definitional tool that is extended, not a uniqueness theorem that forces the abstraction claims. Hyperparameter choices after RQ1 are ordinary experimental selection, not parameters fitted then re-reported as predictions. The acknowledged limitation—that full-model solves are needed to obtain causes—is a practical scalability concern, not logical circularity of the claimed derivation. Score 0; steps empty.

Axiom & Free-Parameter Ledger

3 free parameters · 5 axioms · 3 invented entities

The central claim rests on standard MDP/IMDP/SG semantics, the imported feature-causality definition (sufficiency + subset minimality), the modeling choice that ordinal/categorical predicates over state variables are the right atoms, and several experimental hyperparameters that select which effect sets and iteration depths define ‘the’ causes. No new physical entities; invented objects are definitional (partitions and aggregations).

free parameters (3)
  • relative/percentile threshold ε for Valid/Effect = ε=0.1 (relative) used in main experiments
    Chooses which value band of states counts as Effect vs Valid; fixed after RQ1 (relative ε=0.1 preferred). Directly changes the cause set and partition.
  • number of iterative partition iterations k = k=6
    Controls fineness of C-IT; chosen as k=6 after comparing 6 vs 10 and threshold-based schemes.
  • Effect/Valid semantic configuration (good vs bad bands) = Effect sets 3 and 4 (Fig. 4) for C-1; both good and bad retained for coverage
    Discrete choice among intervals I in Fig. 4; ‘good’ effects preferred post hoc for main runs.
axioms (5)
  • standard math Memoryless deterministic policies suffice for optimality of unbounded reachability/safety on finite MDPs.
    Invoked in §III-A via standard MDP theory [41].
  • domain assumption Feature cause = assignment γ that is sufficient for Effect among Valid and subset-minimal (Def. 4 / [8]).
    Imported wholesale from feature causality; all partitions are built from such causes.
  • domain assumption State variables are ordinal or categorical so Boolean predicates X_i ≥ x or X_i = x form an adequate feature set F_M.
    §IV opening; without meaningful variables the method collapses (authors exclude ‘highly synthetic’ benchmarks for this reason).
  • domain assumption Action-consistency and target-consistency of partitions may be enforced by splitting blocks without harming the intended abstraction use.
    §V-A; simplifies policy transfer and target labeling.
  • ad hoc to paper Exact full-model value analysis to build Effect sets is an acceptable foundational cost; approximation/transfer is future work.
    Stated in Limitations (§I) and Conclusion; load-bearing for the current pipeline’s feasibility narrative.
invented entities (3)
  • One-shot causal partition PredPart (C-1) no independent evidence
    purpose: Group states that agree on the truth of a cause-effect cover.
    Definitional construction from causes; no ontological claim beyond the partition.
  • Iterative causal partition IterPredPart (C-IT) no independent evidence
    purpose: Slice the state space by successive effect sets and stack partial PredPart partitions.
    Algorithm 1; main empirically preferred partition.
  • Property-driven IMDP aggregation of a causal partition independent evidence
    purpose: Lift concrete transitions to interval bounds over abstract blocks.
    Def. 6; authors note independent development but equivalence to discrete transfer of prior interval ideas.

pith-pipeline@v1.2.0-daily-grok45 · 31930 in / 3608 out tokens · 76382 ms · 2026-07-30T21:07:20.181972+00:00 · methodology

0 comments
read the original abstract

Markov Decision Processes (MDPs) are widely used as decision-making models, commonly specified over factored state spaces through state variables and their valuations. The exponential blowup in the number of states renders many reasoning tasks in MDPs challenging. Abstractions are promising techniques to reduce MDPs and thus mitigate scalability issues. In this work, we introduce a notion of causality on factored MDPs and a novel property-driven causal abstraction technique that retains many characteristics of the original MDP model. For this, we rely on causal relations over state variable predicates and identify those states that share the same reasons for fulfilling or violating a given abstraction property. We theoretically and empirically compare various causal MDP abstractions using different model types such as MDPs, interval MDPs, or stochastic games. Our evaluation demonstrates the potential of our approach: For several standard benchmarks, we obtain small abstractions that allow us to compute near-optimal policies for the original MDP. Furthermore, our causal abstractions often generalize to related large-scale MDP models.

Figures

Figures reproduced from arXiv: 2607.26787 by Clemens Dubslaff, David Parker, Jule Schmidt, Maximilian Weininger, Nils Jansen.

Figure 1
Figure 1. Figure 1: The electric taxi MDP model, used as our running [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The property-driven causal abstraction workflow. [PITH_FULL_IMAGE:figures/full_fig_p001_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Predicate partition of the taxi running example. [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Different settings of Effect and Valid for PredPart. however, expensive to compute, since it requires solving the model for the Effect set and computing a minimal covering of Effect. We formalize the suggested minimality characteristic in Remark 1. Remark 1. Given an MDP M and sets Valid and Effect, let C be a minimal covering of Effect w.r.t. Valid. Then, PredPart(M, C) is the coarsest (i.e., lowest cardi… view at source ↗
Figure 6
Figure 6. Figure 6: Example MDP and three possible abstractions after grouping states [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Performance of different causal partitions across benchmarks. [PITH_FULL_IMAGE:figures/full_fig_p008_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Comparing the performance of different abstraction methods. [PITH_FULL_IMAGE:figures/full_fig_p009_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Generalizing causes from the small models to larger model sizes. [PITH_FULL_IMAGE:figures/full_fig_p009_9.png] view at source ↗
Figure 9
Figure 9. Figure 9: Additionally, the appendix compares with medium [PITH_FULL_IMAGE:figures/full_fig_p010_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: MDPs and their WA abstractions to show Item 1 of Theorem 2. [PITH_FULL_IMAGE:figures/full_fig_p013_10.png] view at source ↗
Figure 13
Figure 13. Figure 13: Comparing the best performing threshold-based iter [PITH_FULL_IMAGE:figures/full_fig_p017_13.png] view at source ↗
Figure 11
Figure 11. Figure 11: Performance of different thresholds for the [PITH_FULL_IMAGE:figures/full_fig_p017_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Performance of different iteration types for [PITH_FULL_IMAGE:figures/full_fig_p017_12.png] view at source ↗
Figure 15
Figure 15. Figure 15: Comparison of partitions, including benchmarks where the causal graph retains the original model. [PITH_FULL_IMAGE:figures/full_fig_p018_15.png] view at source ↗
Figure 18
Figure 18. Figure 18: Generalization of causal abstractions. Comparing the [PITH_FULL_IMAGE:figures/full_fig_p018_18.png] view at source ↗
Figure 19
Figure 19. Figure 19: Generalization of causal abstractions. Comparing [PITH_FULL_IMAGE:figures/full_fig_p018_19.png] view at source ↗
Figure 17
Figure 17. Figure 17: Comparison of the performance of different abstrac [PITH_FULL_IMAGE:figures/full_fig_p018_17.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

52 extracted references · 3 linked inside Pith

  1. [1]

    Efficient structure learning in factored-state mdps,

    A. L. Strehl, C. Diuk, and M. L. Littman, “Efficient structure learning in factored-state mdps,” inAAAI, pp. 645–650, AAAI Press, 2007

    2007

  2. [2]

    PRISM 4.0: Verifica- tion of probabilistic real-time systems,

    M. Z. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verifica- tion of probabilistic real-time systems,” inCAV, vol. 6806 ofLecture Notes in Computer Science, pp. 585–591, Springer, 2011

    2011

  3. [3]

    The probabilistic model checker storm,

    C. Hensel, S. Junges, J. Katoen, T. Quatmann, and M. V olk, “The probabilistic model checker storm,”Int. J. Softw. Tools Technol. Transf., vol. 24, no. 4, pp. 589–610, 2022

    2022

  4. [4]

    Construction of abstract state graphs with pvs,

    S. Graf and H. Saidi, “Construction of abstract state graphs with pvs,” in Computer Aided Verification(O. Grumberg, ed.), (Berlin, Heidelberg), pp. 72–83, Springer Berlin Heidelberg, 1997

    1997

  5. [5]

    Alwayssafe: Reinforcement learning without safety constraint violations during training,

    T. D. Sim ˜ao, N. Jansen, and M. T. J. Spaan, “Alwayssafe: Reinforcement learning without safety constraint violations during training,” inAAMAS, pp. 1226–1235, ACM, 2021

    2021

  6. [6]

    Pearl,Causality

    J. Pearl,Causality. Cambridge University Press, 2 ed., 2009

    2009

  7. [7]

    J. Y . Halpern,Actual Causality. The MIT Press, 08 2016

    2016

  8. [8]

    Feature causality,

    C. Dubslaff, K. Weis, C. Baier, and S. Apel, “Feature causality,”J. Syst. Softw., vol. 209, p. 111915, 2024

    2024

  9. [9]

    Bounded-parameter Markov decision processes,

    R. Givan, S. M. Leach, and T. L. Dean, “Bounded-parameter Markov decision processes,”Artif. Intell., vol. 122, no. 1-2, pp. 71–109, 2000

    2000

  10. [10]

    A game- based abstraction-refinement framework for markov decision processes,

    M. Kattenbelt, M. Z. Kwiatkowska, G. Norman, and D. Parker, “A game- based abstraction-refinement framework for markov decision processes,” Formal Methods Syst. Des., vol. 36, no. 3, pp. 246–280, 2010

    2010

  11. [11]

    Eells,Probabilistic Causality

    E. Eells,Probabilistic Causality. Cambridge Studies in Probability, Induction and Decision Theory, Cambridge University Press, 1991

    1991

  12. [12]

    Peters, D

    J. Peters, D. Janzing, and B. Sch ¨olkopf,Elements of Causal Inference: Foundations and Learning Algorithms. Cambridge, MA, USA: MIT Press, 2017

    2017

  13. [13]

    A modification of the halpern-pearl definition of causal- ity,

    J. Y . Halpern, “A modification of the halpern-pearl definition of causal- ity,” inIJCAI, pp. 3022–3033, AAAI Press, 2015. 10

    2015

  14. [14]

    Causality in configurable software systems,

    C. Dubslaff, K. Weis, C. Baier, and S. Apel, “Causality in configurable software systems,” inProceedings of the 44th International Conference on Software Engineering (ICSE), 2022

    2022

  15. [15]

    Sufficient reasons for classifier decisions in the presence of domain constraints,

    N. Gorji and S. Rubin, “Sufficient reasons for classifier decisions in the presence of domain constraints,”Proceedings of the AAAI Conference on Artificial Intelligence, vol. 36, pp. 5660–5667, Jun. 2022

    2022

  16. [16]

    From verification to causality-based explications,

    C. Baier, C. Dubslaff, F. Funke, S. Jantsch, R. Majumdar, J. Piribauer, and R. Ziemek, “From verification to causality-based explications,” inProceedings of the 48th International Colloquium on Automata, Languages, and Programming (ICALP), 2021

    2021

  17. [17]

    Foundations of probability-raising causality in markov decision processes,

    C. Baier, J. Piribauer, and R. Ziemek, “Foundations of probability-raising causality in markov decision processes,”Log. Methods Comput. Sci., vol. 20, no. 1, 2024

    2024

  18. [18]

    Probability-raising causality for uncertain paramet- ric markov decision processes with PAC guarantees,

    R. Oura and Y . Ito, “Probability-raising causality for uncertain paramet- ric markov decision processes with PAC guarantees,” inUAI, vol. 286 ofProceedings of Machine Learning Research, pp. 3300–3321, PMLR, 2025

    2025

  19. [19]

    HyperPCTL: A temporal logic for probabilistic hyperproperties,

    E. ´Abrah´am and B. Bonakdarpour, “HyperPCTL: A temporal logic for probabilistic hyperproperties,” inProc. of the 15th Intern. Conf. on Quantitative Evaluation of Systems (QEST), pp. 20–35, Springer, 2018

    2018

  20. [20]

    Probabilistic Hyperproper- ties of Markov Decision Processes,

    R. Dimitrova, B. Finkbeiner, and H. Torfah, “Probabilistic Hyperproper- ties of Markov Decision Processes,” inProc. of the 18th Intern. Symp. on Automated Technology for Verification and Analysis (ATVA), vol. 12302 ofLNCS, pp. 484–500, Springer, 2020

    2020

  21. [21]

    Causal temporal reasoning for markov decision processes,

    M. Kazemi, J. Lally, and N. Paoletti, “Causal temporal reasoning for markov decision processes,”Research Directions: Cyber-Physical Systems, vol. 3, p. e3, 2025

    2025

  22. [22]

    Probabilistic causes in markov chains,

    R. Ziemek, J. Piribauer, F. Funke, S. Jantsch, and C. Baier, “Probabilistic causes in markov chains,”Innov. Syst. Softw. Eng., vol. 18, no. 3, pp. 347–367, 2022

    2022

  23. [23]

    A survey on causal reinforcement learning,

    Y . Zeng, R. Cai, F. Sun, L. Huang, and Z. Hao, “A survey on causal reinforcement learning,”CoRR, vol. abs/2302.05209, 2023

    Pith/arXiv arXiv 2023

  24. [24]

    Causal reinforcement learning: A survey,

    Z. Deng, J. Jiang, G. Long, and C. Zhang, “Causal reinforcement learning: A survey,” 2023

    2023

  25. [25]

    Bandits with unobserved confounders: A causal approach,

    E. Bareinboim, A. Forney, and J. Pearl, “Bandits with unobserved confounders: A causal approach,” inNIPS, pp. 1342–1350, 2015

    2015

  26. [26]

    Causal based q-learning,

    A. M ´endez-Molina, I. Feliciano-Avelino, E. F. Morales, and L. E. Sucar, “Causal based q-learning,”Res. Comput. Sci., vol. 149, no. 3, pp. 95– 104, 2020

    2020

  27. [27]

    Toward causal-aware RL: state-wise action-refined temporal difference,

    H. Sun, “Toward causal-aware RL: state-wise action-refined temporal difference,”CoRR, vol. abs/2201.00354, 2022

    Pith/arXiv arXiv 2022

  28. [28]

    Causal rein- forcement learning using observational and interventional data,

    M. Gasse, D. Grasset, G. Gaudron, and P. Oudeyer, “Causal rein- forcement learning using observational and interventional data,”CoRR, vol. abs/2106.14421, 2021

    Pith/arXiv arXiv 2021

  29. [29]

    Towards a unified theory of state abstraction for MDPs,

    L. Li, T. J. Walsh, and M. L. Littman, “Towards a unified theory of state abstraction for MDPs,” inAI&M, 2006

    2006

  30. [30]

    Bisimulation through probabilistic testing,

    K. G. Larsen and A. Skou, “Bisimulation through probabilistic testing,” Information and Computation, vol. 94, no. 1, pp. 1–28, 1991

    1991

  31. [31]

    Equivalence notions and model minimization in markov decision processes,

    R. Givan, T. Dean, and M. Greig, “Equivalence notions and model minimization in markov decision processes,”Artificial Intelligence, vol. 147, no. 1, pp. 163–223, 2003. Planning with Uncertainty and Incomplete Information

    2003

  32. [32]

    Metrics for finite markov de- cision processes,

    N. Ferns, P. Panangaden, and D. Precup, “Metrics for finite markov de- cision processes,” inProceedings of the 20th Conference on Uncertainty in Artificial Intelligence, UAI ’04, (Arlington, Virginia, USA), pp. 162– 169, AUAI Press, 2004

    2004

  33. [33]

    Representation discovery for mdps using bisimulation metrics,

    S. S. Ruan, G. Comanici, P. Panangaden, and D. Precup, “Representation discovery for mdps using bisimulation metrics,” inProceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI’15, pp. 3578–3584, AAAI Press, 2015

    2015

  34. [34]

    Pric3: Property directed reachability for mdps,

    K. Batz, S. Junges, B. L. Kaminski, J.-P. Katoen, C. Matheja, and P. Schr¨oer, “Pric3: Property directed reachability for mdps,” inComputer Aided Verification(S. K. Lahiri and C. Wang, eds.), (Cham), pp. 512– 538, Springer International Publishing, 2020

    2020

  35. [35]

    Robust counterfactual inference in markov decision processes,

    J. Lally, M. Kazemi, and N. Paoletti, “Robust counterfactual inference in markov decision processes,” 2026. accepted for publication at AAMAS 2026

    2026

  36. [36]

    Invariant causal prediction for block mdps,

    A. Zhang, C. Lyle, S. Sodhani, A. Filos, M. Kwiatkowska, J. Pineau, Y . Gal, and D. Precup, “Invariant causal prediction for block mdps,” inICML, vol. 119 ofProceedings of Machine Learning Research, pp. 11214–11224, PMLR, 2020

    2020

  37. [37]

    Causal dynamics learning for task-independent state abstraction,

    Z. Wang, X. Xiao, Z. Xu, Y . Zhu, and P. Stone, “Causal dynamics learning for task-independent state abstraction,” inICML, vol. 162 of Proceedings of Machine Learning Research, pp. 23151–23180, PMLR, 2022

    2022

  38. [38]

    Building mini- mal and reusable causal state abstractions for reinforcement learning,

    Z. Wang, C. Wang, X. Xiao, Y . Zhu, and P. Stone, “Building mini- mal and reusable causal state abstractions for reinforcement learning,” Proceedings of the AAAI Conference on Artificial Intelligence, vol. 38, 2024

    2024

  39. [39]

    Test where de- cisions matter: Importance-driven testing for deep reinforcement learn- ing,

    S. Pranger, H. Chockler, M. Tappler, and B. K ¨onighofer, “Test where de- cisions matter: Importance-driven testing for deep reinforcement learn- ing,” inAdvances in Neural Information Processing Systems(A. Glober- son, L. Mackey, D. Belgrave, A. Fan, U. Paquet, J. Tomczak, and C. Zhang, eds.), vol. 37, pp. 28103–28126, Curran Associates, Inc., 2024

    2024

  40. [40]

    M. L. Puterman,Markov Decision Processes: Discrete Stochastic Dy- namic Programming. Wiley Series in Probability and Statistics, Wiley, 1994

    1994

  41. [41]

    Baier and J.-P

    C. Baier and J.-P. Katoen,Principles of model checking. MIT Press, 2008

    2008

  42. [42]

    The complexity of stochastic games,

    A. Condon, “The complexity of stochastic games,”Inf. Comput., vol. 96, no. 2, pp. 203–224, 1992

    1992

  43. [43]

    Strategy synthesis for partially-known switched stochastic systems,

    J. Jackson, L. Laurenti, E. W. Frew, and M. Lahijanian, “Strategy synthesis for partially-known switched stochastic systems,” inHSCC, pp. 6:1–6:11, ACM, 2021

    2021

  44. [44]

    Value iteration,

    K. Chatterjee and T. A. Henzinger, “Value iteration,” in25 Years of Model Checking, vol. 5000 ofLecture Notes in Computer Science, pp. 107–138, Springer, 2008

    2008

  45. [45]

    Robust dynamic programming,

    G. N. Iyengar, “Robust dynamic programming,”Mathematics of Oper- ations Research, vol. 30(2), pp. 257–280, 2005

    2005

  46. [46]

    Implicit and incremental computation of primes and essential primes of boolean functions,

    O. Coudert and J. C. Madre, “Implicit and incremental computation of primes and essential primes of boolean functions,” inDAC, pp. 36–39, IEEE Computer Society Press, 1992

    1992

  47. [47]

    The revised practitioner’s guide to MDP model checking algorithms,

    A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “The revised practitioner’s guide to MDP model checking algorithms,”Int J Softw Tools Technol Transfer, 2026. 11 APPENDIXA PROOFS FORSECTIONIV A. Proof of Theorem 1 Intuitively, Theorem 1 claims that for a given MDPM withValid,Effect, and a cause-effect coverC, the cardinality ofPredPart(M, C)is alwa...

    2026

  48. [48]

    Then, by definition,f i,k ̸⊂γ, k∈[1..|X i|, γ∈C]

    Leti∈I irr be the index of an irrelevant feature. Then, by definition,f i,k ̸⊂γ, k∈[1..|X i|, γ∈C]. Otherwise, it would violate Definition 4, Item(C2). LetS CG ∈ CGPart(M, Iirr). By definition,∀s,s ′ ∈ SCG, the states only differ in irrelevant features, i.e.,∀i∈[1..n]\I irr : x ′ i =x i. Hence,γ(s) =γ(s ′)forallγ∈C, i.e.,s,s ′ are in the sameS P ∈PredPart...

  49. [49]

    If someS P ∈PredPart(M, C)is a superset of mul- tipleS CG ∈CGPart(M, Iirr), then|CGPart(M, I irr)|> |PredPart(M, C)|

    If for all setsS CG there is a setS P such that SCG =S P , then|CGPart(M, Iirr)|=|PredPart(M, C)|. If someS P ∈PredPart(M, C)is a superset of mul- tipleS CG ∈CGPart(M, Iirr), then|CGPart(M, I irr)|> |PredPart(M, C)|. APPENDIXB PROOFS FORSECTIONV A. Proof of Theorem 2 - Item 1 We show that theWAabstraction can lead to arbitrarily wrong values using the cou...

  50. [50]

    We show that there exist interval policiesπ 2 that induce probability distributions giving upper and lower bounds on the values of the original MDP in Lemma 1

  51. [51]

    Then, we show that these interval distributions belong to MDPs consistent with the IMDP in Lemma 2

  52. [52]

    good” compared to “bad

    Finally, we use these findings together with Remark 6 and Remark 7 to prove the inequalities of Item 2 by induction. The proof is analogous for all four inequalities. We include the full proof foropt = max,W(ˆs)≤V(s)and point out the differences where applicable for the three remaining cases. Necessary lemmas and their proofs. Lemma 1.There exist interval...