Formal Methods in Computer-Aided Design 2026
Property-driven Causal Abstractions for Markov Decision Processes Jule Schmidt1 , Maximilian Weininger1 , Clemens Dubslaff2 , David Parker3 , Nils Jansen1,4 {jule.schmidt, maximilian.weininger, n.jansen}@rub.de, [email protected], [email protected] 1 Ruhr-University Bochum, Germany, 2 Eindhoven University of Technology, The Netherlands,
arXiv:2607.26787v1 [cs.AI] 29 Jul 2026
3 Oxford University, UK, 4 Radboud University, Nijmegen, The Netherlands
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.
I. I NTRODUCTION Markov Decision Processes (MDPs) are a common model for sequential decision-making under uncertainty. A standard way to specify an MDP is by factoring its state space, where each state corresponds to a valuation of a vector of state variables [1]. These variables inherently carry meaning, capturing structural properties of the environment and providing a compact description of the system dynamics. Probabilistic model checking tools like PRISM [2] or Storm [3] have input languages that follow this principle and provide mature implementations for formally analyzing MDPs. Abstractions. As the number of variables increases, the induced state space quickly grows beyond the reach of exact analysis, which motivates the use of abstractions. Abstractions reduce the size of the original MDP model, simplifying the solving while preserving the information relevant to the property of interest. Predicate abstraction [4] groups states according to the truth values of predicates over the state variables. However, choosing suitable predicates is difficult, domain-dependent, and may result in abstractions that are either still too large to be solved or too coarse to be informative. Example 1. Throughout this paper, we use the electric taxi MDP [5], visualized in Fig. 1, as our illustrative running example. In brief, the taxi must navigate a 2D grid-world, to bring a passenger to a destination, while ensuring that it does not run out of battery. Passing by a charging station
https://doi.org/
y
x 0
0
♀
c
1
C
2
1 2
Fig. 1: The electric taxi MDP model, used as our running example throughout the paper.
MDP Property
Analysis
Effect
Causal Reasoning
Causal Partition
Aggregation
Abstraction
Fig. 2: The property-driven causal abstraction workflow.
allows the battery to be recharged. Already for a 3 × 3 grid, this MDP consists of 93 states. A grid of size 10 × 10 has ca. 8200 states, a 100×100 grid has ca. 107 , and even larger state spaces are to be expected in real-world scenarios. Many states, however, carry similar information: For example, the agent’s grid position can be identical across different battery levels and regardless of the passenger’s status. Slightly different position valuations may also induce the same level of safety criticality. An abstraction only focused on safety can merge these states, leaving a smaller model for exact analysis. Causality. The example illustrates that property-relevant information often depends on concrete valuations of specific state variables only. To reveal such information, we employ approaches from causal inference [6], [7]. In our context of MDPs, such reasoning helps identify state variables and valuations that cause the satisfaction or violation of a property. Our approach: Property-driven causal abstractions. We provide formal concepts of causality for factored MDPs, establishing feature causality [8] over state variable predicates. We develop abstraction methods that (1) find causes for a given property of interest in a factored MDP, (2) use these causes to obtain state-space partitions, from which we (3) construct abstract models that provide a suitable tradeoff between model size and preservation of property-relevant information. We
This article is licensed under a Creative Commons Attribution 4.0 International License
now detail the steps of our approach as visualized in Fig. 2. Effect sets and predicates. In the first step, we analyze the input MDP regarding the property at hand, such as reaching certain unsafe states. Based on that, we build so-called effect sets that distinguish states with respect to (potentially multiple different) probabilities to satisfy (“good effects”) or violate (“bad effects”) the property, or more fine-grained notions such as nearly satisfying or violating. Then, we employ a Boolean encoding of the factored state towards a predicate abstraction describing the membership of states to the various effect sets. Causes. The second step introduces the novel concept of feature causality for factored MDPs. Our notion of causes takes into account specific valuations of state variables and not just the states, exploiting the inherent meaning of variables. Using causal inference, we determine such causes as minimal sets of predicates sufficient to show an effect. Causal partition. We then partition the state space based on causally relevant parts. In particular, we consider three approaches towards such a partition: one-shot, which groups states that satisfy the same causes; iterative, which iteratively considers multiple effect sets; and causal graph, a standard way to aggregate states that neglect specific state valuations. Abstraction. Given a partition and the original MDP, we finally build an abstraction by aggregating states in the same subset of the partition into one abstract state. To achieve a thorough evaluation of the approach, we compare three methods for abstracting an MDP’s transition function: (1) using a weighted average, resulting in an MDP [5], (2) constructing an interval MDP where the intervals capture all possible transition probabilities [9], and (3) using a stochastic game where an opponent chooses original states from the partition [10]. Results. Our paper introduces property-driven causal abstractions and demonstrates their potential: Our experimental evaluation shows that, on many models, causal abstractions reduce model size, while hardly compromising the quality of optimal policies. Further, causes can generalize from small model variants to larger ones. Our detailed analysis of different choices in analyzing the property, performing causal reasoning, and aggregating states reveals that usually, focusing on states that are close to satisfying the property leads to the best partitions, and that using SG-based abstractions leads to the best performance. Overall, our contributions are the following: • A new notion of causality exploiting the meaning of state variables in factored MDPs. • Property-driven causal abstractions, including interval MDPs, and their theoretical analysis. • An empirical evaluation of the tradeoff between abstraction and policy performance on standard benchmarks. Limitations. Currently, our approach requires expensive steps, namely analyzing the whole MDP to find effect sets and computing the causes. However, our main goal is to achieve a fundamental understanding of feature causality and its potential for abstracting MDPs. Then, given this knowledge, the next step is to develop efficient ways to approximate the effect set and its causes, for example by reinforcement learning or by solving small MDPs precisely to obtain causes and then
using them to abstract larger model variants. We remark that no automated abstraction method can be expected to work for every MDP, independent of property and structure. We view our approach as a step on the route towards scalability instead of a complete practical solution. II. R ELATED W ORK Causality has been extensively studied in philosophy, social sciences, and artificial intelligence [11], [6], [12]. Seminal work by Halpern and Pearl led to actual causality [13] establishing cause-effect relationship-based structural causal models (SCMs). Feature causality [14] is a form of actual causality that does not rely on learning SCMs [8] and can serve as abductive explanations under constraints [15]. Our approach relates most to work on causal reasoning in Markovian models, recently considered in formal verification and reinforcement learning (RL). Probabilistic causes were defined as state sets for which the probability of an effect increases [16], [17], [18]. Other approaches rely on hyperproperties [19], [20], using counterfactual logic [21], or smallest prefix paths [22]. Due to their path dependency, they are not directly suitable for local causal state abstractions as we present here. In the context of RL, causal information is mainly used to improve the performance —cf. surveys on causal RL [23], [24]. Most approaches there rely on given SCMs and adapt existing model-free [25], [26] and model-based methods [27], [28]. Abstracting Markovian models. Various state-abstraction and refinement methods tackle the state-space-explosion problem in MDP-based analysis [29]. Probabilistic bisimulation [30] is prevalent, which has been extended to MDPs with factored state spaces [31] or using bisimulation metrics [32], [33]. PrIC3 [34] uses on-the-fly abstraction and refinement in MDPs but does not exploit factored information. Simão et al. considered abstractions in constrained factored MDPs during RL at the level of variables [5]. Our abstraction method is more fine-grained, relying on variable valuations and their impact. Causal abstractions. Lally et al. [35] consider causal abstractions towards interval MDP with theoretical guarantees, however relying on SCMs compatible with an underlying MDP. Zhang et al. [36] identify causal state features in socalled block MDPs using invariant causal prediction to improve RL but rely on different notions of causality depending on conditional probabilities. Another line of work learns causal graphs over state variables to derive abstractions [37], [38]. Clustering states in an MDP with similar causal importance for an RL objective has shown to improve learning [39]. Similarly, we propose a property-driven abstraction method lumping explanatory equivalent states. In contrast to the aforementioned abstraction approaches, we provide a foundational formal framework for property-driven causal abstraction in factored MDPs that does not rely on SCM learning, statistical data, nor is limited to the application of RL. III. P RELIMINARIES We recall Markov decision processes (MDPs, Section III-A) and their extensions to interval MDPs and stochastic games
2
(Section III-B) that we use for abstractions. Finally, we provide the basic notions of feature causality (Section III-C). For bounds ℓ, u ∈ N, let us denote by [ℓ..u] the interval {n ∈ N | ℓ ≤ n ≤ u}. Given a finite set Y , a partition of Y is a set U P = {P1 , . . . , Pk ⊆ Y } of pairwise disjoint sets such that i∈[1,k] Pi = Y . A probability distribution over Y is a P function d : Y → [0, 1] where y∈Y d(y) = 1. The set of all probability distributions over Y is denoted by D(Y ), and Y ω is the set of all infinite sequences of elements in Y .
B. Interval Markov Decision Processes and Stochastic Games Definition 2 (Interval MDP (IMDP)). An IMDP [9] is a tuple M = (S, A, PL , PU ), where S and A are as for MDPs and PL , PU : S × A × S → [0, 1] are functions providing lower and upper bounds on transition probabilities. We write M ∈ M to indicate that an MDP M is consistent with an IMDP M. That is, they share state and action spaces, and for all states s, s ′ and actions a we have PL (s, a, s ′ ) ≤ P(s, a, s ′ ) ≤ PU (s, a, s ′ ) Note that if PL (s, a, s ′ ) > PU (s, a, s ′ ), there exists no consistent MDP.
A. Markov Decision Processes Definition 1 (Markov decision process (MDP)). An MDP [40] is a tuple M = (S, A, P) with finite sets of states S and actions A, and a (partial) transition function P : S × A → D(S).
Example 4. Recall from Example 2 that the chances of being stuck in traffic are precisely known to be 0.1. In an IMDP, we can instead have, e.g., P(s0 , l, s1 ) = [0.8, 0.95] and P(s0 , l, s2 ) = [0.05, 0.2], adding uncertainty to the transition probability. In Section V, we will abstract IMDPs from MDPs by grouping states. Then, the bounds on the transition probabilities are determined by the extremal transition probabilities in the group of states.
We say that an MDP M = (S, A, P) is factored if every state s ∈ S is a vector of n state valuations (x1 , . . . , xn ) ∈ X1 × . . . × Xn over state variables Xi associated with a finite domain of mi elements xi,j for i ≤ n, j < mi . We write A(s) for the set of available actions in state s ∈ S, i.e., those where P is defined, and assume A(s) ̸= ∅ for all s ∈ S. We write P(s, a, s ′ ) for P(s, a)(s ′ ).
IMDP semantics and value. The semantics of an IMDP is the set of all consistent MDPs. We focus on consistent MDPs with best- and worst-case value: For a given optimization direction opt ∈ {min, max}, we write opt for its complement, i.e., opt := min if opt = max and opt := max otherwise. Then, BM (s) := optM∈M VM (s) and WM (s) := optM∈M VM (s) are the best- and worst-case value of a state s, respectively.
Example 2. We model the taxi example from the introduction (see Fig. 1) as the following MDP: The state space is made up of four state variables X1 × X2 × X3 × X4 ∈ [0..2] × [0..2] × [0..5] × {0, 1}, with two variables for the position, one for the battery, and one for the passenger’s status. The actions are A = {u, d, l, r, e}, where the first four move the taxi up, down, left, or right, and e allows the passenger to enter or exit the taxi. Action e is only available in states with battery > 0 at the pickup location (x = 0, y = 0). For a moving action, the transition function P(s, a) assigns probability 0.9 to the state in the chosen direction and probability 0.1 of getting stuck in traffic; in both cases, the battery decharges. States with battery = 0 are self-looping sink states, and the taxi resets battery to 5 by passing the charging station at x = 2, y = 2.
Definition 3 (Stochastic game (SG)). An SG [42] is a tuple G = (S, S△ , S▽ , A, P), where S, A, and P are as for MDPs and S = S△ ⊎ S▽ , i.e., the state space is partitioned into states of the agent (△) and opponent (▽). SG semantics and value. In SGs, we separately consider the sets of policies Π△ and Π▽ of the agent and opponent, where π△ ∈ Π△ is a function S△ → A and analogously for the opponent. Fixing a pair of policies (π△ , π▽ ) induces π△ ,π▽ as in MDPs. The value of a a probability measure Ps,G △ ,π▽ state is VG (s) := optπ△ ∈Π△ optπ▽ ∈Π▽ Pπs,G [♢T]. We additionally define an analogue of the best-case value of IMDPs, where the opponent states also play in favour of the agent: △ ,π▽ BG (s) := optπ△ ∈Π△ optπ▽ ∈Π▽ Pπs,G [♢T].
The semantics of MDPs is defined as usual through policies and paths. A policy is a function π : S → A assigning to each state s an available action a ∈ A(s). We restrict to memoryless deterministic policies , as these suffice for optimality under the objectives we consider [41]. A path is an infinite sequence ρ = s0 a0 s1 a1 . . . ∈ (S × A)ω where P(si , ai , si+1 ) > 0 for all i ∈ N0 . We write ρi for the state si of a path ρ. Π is the set of all policies and PathsM the set of all paths. Applying a policy π to an MDP M induces for each state s a unique probability measure over paths Pπs,M [41, Chapter 10.1]. Property, objective and value. A reachability property combines a set of target states T ⊆ S with an optimization objective opt ∈ {min, max} that captures the optimal probability to reach T, denoted ♢T := {ρ ∈ PathsM | ∃i ∈ N0 : ρi ∈ T}. The value of a state s is VM (s) := optπ∈Π Pπs,M [♢T].
C. Feature Causality Feature causality [8] reasons about Boolean features and their influence on properties. For features F , let F = {a, a | a ∈ F } denote the set of literals indicating that a feature a is active (a) or inactive (a). An assignment δ ⊆ F is a set of literals where no feature occurs twice, called total if every feature occurs exactly once. We denote by ∆(F ) and Θ(F ) the set of assignments and total assignments, respectively. The semantics JδK of an assignment δ is the set of consistent total assignments, i.e., JδK := {θ ∈ Θ(F ) | δ ⊆ θ}. Let Valid ⊆ Θ(F ) be the set of valid assignments satisfying domain constraints, and Effect ⊆ Valid a set of effect assignments. The goal is now to determine those assignments that are sufficient to guarantee an effect among those that are valid.
Example 3. An example property for the taxi model uses opt = min and T = {(x , y, battery, passenger ) | battery = 0}. Intuitively, the value of a state captures the minimum probability for it to run out of battery.
3
Definition 4 (Cause [8]). Let Effect ⊆ Valid ⊆ Θ(F ). A cause of Effect w.r.t. Valid is an assignment γ ∈ ∆(F ), where (C1) ∅ ̸= JγK ∩ Valid ⊆ Effect (sufficiency) (C2) JδK ∩ Valid ⊈ Effect for all δ ⊂ γ (subset minimality).
Inspired by actual causality [7], (C1) implements the sufficiency condition, ensuring that all total assignments from γ are in Effect, and (C2) ensures subset minimality. A cause γ thus can serve as explanation for any assignment θ ∈ JγK ∩ Effect. Causes is the set of all causes of Effect w.r.t Valid. Cause-effect covers. A cause-effect cover is a set of causes C S ⊆ Causes that explain the whole set Effect, i.e., Effect ⊆ γ∈C JγK. We call C a minimal covering if there is no causeeffect cover C ′ where |C ′ | < |C| [8, Section 4.2]. Computing an exact minimal covering is expensive, therefore heuristics based on most general causes [8, Definition 4] are used to establish small cause-effect covers.
Fig. 3: Predicate partition of the taxi running example.
IV. C AUSAL PARTITIONS FOR FACTORED MDP S In this section, we establish several approaches to derive partitions of MDP state spaces using property-driven causal predicates. We thereby define the concept of feature causality for MDPs. We fix a factored MDP M = (S, A, P) and introduce predicates over its state variables Xi as a basis for predicate abstractions of its state space S. We assume that state variables Xi are either ordinal or categorical. Ordinal variables are interpretable with a meaningful order, like a coordinate of a grid position. Let O ⊆ [1..n] be the index set of all ordinal state variables in M. Categorical state variables represent distinct categories like the color of a signal.
Example 5. In our taxi MDP running example, all state variables are ordinal. We focus here on the battery: if battery = 3, that implies battery ≥ 2, battery ≥ 1, and battery ≥ 0. In our definition of taxi, the domain of this variable is battery ∈ [5]. Therefore, we get five boolean variables: fbattery,k , k ∈ [1..5]. For states in which battery = 3, these are assigned as follows: fbattery,k = 1, k ∈ {1, 2, 3} and fbattery,k = 0, k ∈ {4, 5}. B. One-shot Causal Partition We propose a partition technique that is conceptually simple yet powerful. For an MDP M and a set of predicate assignments C ⊆ ∆(FM ), our partition groups states that are in the semantics of the same subset of assignments. We refer to the partition algorithm as PredPart, as it is well-defined independent of the method used to generate C. As we use causal predicates, and the input is exactly one set of predicates C, we call partitions generated using PredPart one-shot causal partitions, abbreviated to C-1 in the evaluation. We define:
A. Predicate Abstraction for Factored MDPs We define a set of Boolean features, one for each state variable valuation except the smallest one in ordinal variables, called FM . Here, every state s ∈ S uniquely corresponds to a total assignment θs ∈ Θ(FM ). Hence, the semantics of an assignment over the features FM corresponds to a set of states in M. We refer to the Boolean features as fi,k where i is the index of the state variable Xi and k ∈ [0..|Xi |] its k-th valuation. For an ordinal state variable Xi we assume the order xi,j ≤ xi,k iff j ≤ k. We now describe sets of states through assignments over FM modulo a theory over ordinal and categorical predicates. [ FM = fi,k | k ∈ [0..mi ] \ fi,0 | i ∈ O .
PredPart(M, C) = {{s ′ ∈ S | ∀δ ∈ C : δ(s ′ ) = δ(s)} | s ∈ S} Example 6. Fig. 3 shows a predicate partition of the taxi MDP, in three dimensions (x, y, and battery) as the passenger is causally irrelevant. Circles represent states in the original MDP, and colors indicate partition subsets. For subset 0, the predicate is (battery ≥ 1) ∧ (x ≥ 2) ∧ (y ≥ 2), which covers all states where x and y are 2, and the battery level is ≥ 1.
i∈O
Let s = (s0 , . . . , sn ) be a concrete state in M. The interpretation of state s, θs , distinguishes ordinal and categorical features: If Xi is ordinal, then we define fi,k = 1 if si ≥ xi,k and fi,k = 0 otherwise. That means that fi,k is interpreted as a predicate Xi ≥ xi,k . Note that binary variables Xi with domain {0, 1} are covered by our definition of ordinal features. In this case, we simplify notation and write Xi instead of Xi ≥ 1. If Xi is categorical, then fi,k = 1 iff si = xi,k , i.e., fi,k is interpreted as a predicate Xi = xi,k . Given an assignment δ ∈ ∆(FM ) and a state s, we write δ(s) = 1 if θs is in the semantics of δ, and otherwise δ(s) = 0.
When we use the partition as input for aggregations (Section V), its size determines the size of the abstract model. There are at most 2|C| groups in a PredPart partition, if the semantics of every combination of assignments are not empty. If C is a minimal cause-effect cover, the size of the partition is minimal and still fully covers Effect. That means when PredPart is used with a minimal cause-effect cover, it is optimal in size and thus serves as a theoretical milestone of what causal partitions can achieve in terms of size. It is,
4
Fig. 4: Different settings of Effect and Valid for PredPart. Ek
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 cardinality) causal partition induced by Valid and Effect. This follows directly from the definition of minimal coverings.
...
E2
E1
E0
Fig. 5: Visualization of the intuition for IterPredPart.
done by solving multiple reachability queries, where the previous iteration’s Effect set becomes the next target set. Formally, for k iterations, with a threshold τ and starting from states of value 1, the initial sets are Effect0 = {s ∈ S | V(s) = 1} and Valid0 = S. Then, for the following iterations: Effecti = {s ∈ S | Ps (♢Effecti−1 ) > τ }, i ∈ [1, k]
Choosing assignment sets. The Valid and Effect sets determine the state space partition and are built according to the given property and objective, such as the minimal reachability probability. The property induces a value for each state, and we use different thresholds on those values to partition states into the Valid and Effect sets. We consider percentile and relative thresholds. For percentile thresholds, ε fixes the percentage of states to include. For example, if ε = 0.1, and the 10% of states with lowest value have V(s) ≤ 0.25 and the highest 10% have V(s) ≥ 0.93, then we use those values as thresholds τ0 and τ1 . Relative thresholds depend not only on ε, but also the value of a state of interest s0 , e.g. an initial state. Then, the relative threshold is τ = V(s0 ) · (1 ± ε). For example, if V(s0 ) = 0.5 and ε = 0.1, we get lower and upper relative thresholds τ0 = 0.45 and τ1 = 0.55. Next to the thresholds, we also consider different ways to use them to construct Valid and Effect. For Valid, we can either use all reachable states as Valid = {θs ∈ Θ(FM ) | s ∈ S : s is reachable} (Valid 0 in Fig. 4), or exclude states with values larger (Valid 2) or smaller (Valid 1) than τ . Further, we formalize the Effect set using the predicates in FM : Given an interval I ⊆ [0, 1], Effect(I) = {θs ∈ Θ(FM ) | V(s) ∈ I}. Fig. 4 shows different effect sets for intervals under two thresholds τ0 and τ1 , e.g., Effect 4 is provided by I4 = [0, τ1 ).
Validi = Validi−1 \Effecti−1 From the iterative Valid and Effect sets and the MDP, we obtain a list of sets of causes. We use this list in Algorithm 1 to construct the iterative partition, called C-IT. For each slice, it generates a partial partition like PredPart, retaining states outside Effect for future iterations. The resulting partition is more fine-grained than PredPart. Algorithm 1 Deriving the iterative causal partition. procedure G ET C-IT(MDP M, cause list CS) P =∅ S′ = S for all C in CS do P = P ∪ {{s ′ ∈ S ′ | ∀δ ∈ C : δ(s ′ ) = δ(s) ∧ ∃δ ∈ ′ C : δ(s ) = true} | s ∈ S ′ } S ′ = S ′ \{s ∈ S ′ | ∃δ ∈ C : δ(s) = true} end for if |S ′ | > 0 then P = P ∪ {S ′ } end if return P end procedure Choosing iterative assignment sets. There are several ways to define iterations over Valid and Effect sets. One option is to fix a threshold as for PredPart, and re-use it for future iterations on new Effect sets. Alternatively, we predefine a desired number of k iterations, adapt thresholds dynamically, and recursively split by the median value of remaining states.
Example 7. For an MDP with a reachability property and maximizing objective, Valid 1 in Fig. 4 excludes the “worst”, and Valid 2 the “best” states. Effect 0 and 4 capture “bad” states. The meaning of Effect 2 depends on Valid. For the specific example in Fig. 3, we consider a “good” Effect set with Valid 0 and Effect 3.
D. Causal Graph Partition C. Iterative Causal Partition
Traditionally, causality captures dependencies between features, which are visualized in causal graphs as edges between causally dependent features. These dependencies are usually assumed to be given or estimated from data using statistical causal discovery methods. Here, we can omit those estimations since we have access to the full model. Intuitively, a causal
Abstractions built from PredPart tend to be small and to fixate on states with extreme values, motivating more elaborate approaches. We propose to iteratively consider finer slices of the state space as Effect, compute causes for each, and build a partition from the causal slices, as shown in Fig. 5. This is
5
graph partition ignores features that do not cause any part of the effect. Using this information, we build a causal graph and identify the indices of irrelevant features Iirr ⊆ [1..n]. Then, CGPart groups states that only differ in irrelevant features:
The SG abstraction (Fig. 6d) frames the abstract model as a 2-player game. Abstract states belong to the opponent and offer a choice of multiple successor states (gray squares). Each of these states corresponds to a set of original states that have equivalent outgoing distributions for each action. Here, states CGPart(M, Iirr ) = {{s ′ ∈ S | ∀i ∈ [1..n]\Iirr : si′ = si } | s ∈ S} q and r behave differently, resulting in two choices in {q, r}. Given the MDP M and Effect, CGPart is always at least as Action- and target-consistent partition. Before formally definlarge as a corresponding PredPart, formalized as follows. ing the aggregation methods, we provide two notions that simTheorem 1. Given an MDP M with sets Valid and Effect, a plify the definitions. Action-consistency requires that all states cause-effect cover C of Effect w.r.t. Valid, and Iirr the irrele- s in an abstract state ŝ share the same set of available actions. vant features given the causal graph for M and Effect. Then, This set then constitutes the set of available abstract actions ∀SCG ∈ CGPart(M, Iirr ) : ∃SP ∈ PredPart(M, C) : SCG ⊆ Â(ŝ), i.e., A(s) = Â(ŝ). This simplifies transferring policies SP . Thus, |CGPart(M, Iirr )| ≥ |PredPart(M, C)|. between abstraction and original model. The assumption is Proof sketch. The first claim follows from Definition 4: An easily satisfied by refining any given partition P to be actionirrelevant feature cannot appear in any cause. The second claim consistent by splitting groups of states into new sets that agree on their available actions. Formally, for every subset ŝ ∈ P follows from the first. Appendix A provides the full proof. and original state s ∈ ŝ, the refined partition contains the set Remark 2 (Inputs to the partition algorithms). Under the same {s ′ ∈ ŝ | A(s ′ ) = A(s)}. Related work often assumes that all hyperparameters, all three partitions are based on, or start actions are available in all states [43], [5]. from, the same set of input causes. Specifically, the set C Similarly, we require target-consistency, i.e., no subset of of predicate assignments used for the one-shot partition is the the partition contains both target and non-target states. While set of causes that is obtained automatically using one Effect it is possible to soundly define the abstractions without this set. The same set C is used to derive the irrelevant features requirement, target-consistency simplifies the definitions (an for the causal-graph partition. Further, C is the first iteration abstract state ŝ is a target iff ŝ ⊆ T). Target-consistency is step for threshold-based iterative partitions. implicitly ensured in [5] and explicitly required in [10], [43]. V. F ROM PARTITION TO A BSTRACTION Definition 5 (Weighted Average (WA) Abstraction). For a P Given an MDP and a state space partition, we construct an abstract model via an aggregation method. This method maps each subset of the partition to a single abstract state and induces an abstract transition function that approximates the original. Section V-A provides three such methods: the weighted average method (WA) averages transition probabilities of aggregated states (Definition 5); the IMDP method represents all possible transition probabilities as an interval (Definition 6); and the SG method lets an opponent player choose an original state from an abstract one (Definition 7). Section V-B discusses (dis-)advantages of these methods.
and MDP M = (S, A, P), the weighted average abstract MDP is M̂ = (Ŝ, Â, P̂) with: Ŝ = P ,  = A and for all s ∈ ŝ, A(ŝ) = A(s). For ŝ, ŝ ′ P ∈ Ŝ and P a ∈1 Â(ŝ), the′ transition P(s, a, s ). function is P̂(ŝ, a, ŝ ′ ) = s∈ŝ s ′ ∈ŝ ′ |ŝ| Definition 6 (IMDP Abstraction). For P and MDP M = (S, A, P), the abstract IMDP is M̂ = (Ŝ, Â, PL , PU ) with Ŝ, and  as in Definition 5. For ŝ, ŝ ′ ∈ Ŝ and a ∈ Â(ŝ), the lower and upper bounds P on the transition probabilities are P̂L (ŝ, a,P ŝ ′ ) = mins∈ŝ s ′ ∈ŝ ′ P(s, a, s ′ ) and P̂U (ŝ, a, ŝ ′ ) = maxs∈ŝ s ′ ∈ŝ ′ P(s, a, s ′ ). While the definitions of WA and IMDP abstraction follow naturally from Example 8, formally capturing the idea of the SG abstraction is more involved. We introduce the following notation: P PP (s) = ′ {(a, d) | a ∈ A(s), d ∈ D(P ) : d(ŝ) = s ′ ∈ŝ P(s, a, s )}, i.e., PP (s) is the set of all action-distribution pairs available in s, where d is the transition function lifted to the partition. For example, in Fig. 6d, we have PP ({q, r}) = {(b, [{s} 7→ 0.1, {t, u} 7→ 0.9]), (b, [{t, u} 7→ 1]}. The subsets of the partition correspond to opponent states, where first, the opponent chooses an original state, and then the agent chooses an action (and a distribution over successor states). Thus, the agent states merge all original states that have the same action-distribution pairs.
A. Aggregation Methods Example 8. We start with an example to provide the intuition for the three aggregation methods and showcase their differences. Consider the MDP in Fig. 6a and a partition that groups {q, r} and {t, u}, but leaves all other states as singletons. In all three abstractions, this partition forms the abstract state space, and successor distributions are aggregated by summing across concrete states in an abstract state. The WA abstraction (Fig. 6b) obtains transition probabilities from an abstract state by averaging the probabilities of the concrete states. E.g., P̂({q, r}, b)({s}) = 21 ·0.1+ 12 ·0 = 0.05. The IMDP abstraction (Fig. 6c) obtains transition probabilities via the minimum and maximum of the probabilities of its concrete states. When taking action b in {q, r}, the probability for {s} is in [0, 0.1] and for {t, u} is in [0.9, 0.2 + 0.8] = [0.9, 1]. As we prove in Section V-B, the best- and worst-case value of the IMDP always contains the original MDP’s value.
Definition 7 (SG Abstraction). For P and MDP M = (S, A, P), the abstract SG is Ĝ = (Ŝ, Ŝ△ , Ŝ▽ , Â, P̂) with Ŝ▽ = P and Ŝ△ = {PP (s) | s ∈ S}. Â = A ∪ Ŝ△ , where for ŝ ∈ Ŝ▽ , we have A(ŝ) = {PP (s) | s ∈ ŝ}, and picking the ac-
6
{p} a
0.
b
b
0. 2
0. 05
{s}
a
{t, u}
{s}
(b) WA
1
{q, r}
] ,1 .9 [0
(a) MDP
u
95 0.
t
8 0.
s
{q, r}
b 9 0.
0. 1
b
{q, r}
0. 1]
r
{p}
[1, 1]
1
5
q
{p} a
[0 ,
0. 5
a
{t, u} (c) IMDP
b 0.1
p
0.9
{s}
b 1
{t, u} (d) SG
Fig. 6: Example MDP and three possible abstractions after grouping states {q, r} and {t, u}: (a) Original MDP; (b) weighted average (WA) MDP abstraction; (c) IMDP abstraction; (d) SG abstraction. tion surely leads to the selected successor, i.e., P̂(ŝ, Y, Y ) = 1 for Y ∈ Ŝ△ . For Y ∈ Ŝ△ , recall that Y is a set of actiondistribution pairs (a, d). Then, A(Y ) = {a | (a, d) ∈ Y }, and for ŝ ∈ Ŝ▽ we have P̂(Y, a, ŝ) = d(ŝ).
reachability probabilities in abstract states are strictly smaller or larger than in the original MDP. For the IMDP abstraction, we first show that there exist valid probability distributions giving upper and lower bounds on the values of the original MDP that are consistent with the IMDP. We then use an inductive argument to prove the relevant inequalities. For the SG abstraction, the proof from [10, Theorem 1] still applies to our definition.
Definition Origins. The WA abstraction originates from [5]. We developed the IMDP abstraction independently, but it is effectively equivalent to transferring [43, Eqs. (5) and (6)] to the discrete setting. The SG abstraction adapts [10] to our notation, in particular adding action identifiers. The definitions do not require the given partition to be causal.
From a practical perspective, the value problem for all three models used as abstractions can be solved efficiently with dynamic programming: value iteration [44], [42] for MDPs or SGs; and robust value iteration [45] for IMDPs. Despite the differences in the underlying models, the efficiency and scalability of these solution methods are relatively similar.
B. Theoretical Comparison of Aggregation Methods We compare the aggregation methods with respect to three measures of quality: (i) size, (ii) value bounds, i.e., how the value(s) of the abstraction relate to the original MDP’s value, and (iii) policy performance, i.e., how a worst-case optimal policy in the abstraction performs in the original MDP. Abstraction size. Effectively, all abstractions are of the same size with an abstract state for every subset of the partition. The SG abstraction contains the additional agent states, but they need not be stored explicitly, as there is a strict alternation between states of agent and opponent [10, Section 3]. Value bounds. The WA abstraction does not provide any precision indication and the abstract MDP’s value can be arbitrarily smaller or larger than the original MDP’s. In contrast, the IMDP and SG abstraction yield an interval with a best- and worst-case value that is guaranteed to contain the original MDP’s value. The width of the interval is then a measure of their precision. We summarize these insights in Theorem 2, where ⪯ indicates ≤ for max and ≥ for min objectives.
Policy performance. An abstract policy can be applied in the original MDP as follows: For a policy π̂ in the abstract MDP or IMDP, we obtain a policy π for the original MDP by setting π(s) = π̂(ŝ) for every original state s, where ŝ is the unique state with s ∈ ŝ. For a policy in the abstract SG, every agent state corresponds to a set PP (s). Thus, we can transfer an abstract agent-policy in the SG to the MDP by selecting the action chosen in the unique abstract agent state corresponding to the original s. As the abstractions differ widely in how they aggregate information, the policy performance on the original MDP can also differ depending on the MDP’s structure and the given partition, as empirically demonstrated in Section VI. VI. E XPERIMENTAL E VALUATION Our evaluation focusses on the following questions: (RQ1) How does the property affect performance? (RQ2) How do different causal partitions compare? (RQ3) How do different aggregation methods compare? (RQ4) Do the causal partitions generalize to larger models?
Theorem 2. For MDP M and partition P , let M̂, M̂, and Ĝ be the abstract MDP, IMDP, and SG according to Definitions 5 to 7. For every abstract state ŝ ∈ P and original state s ∈ ŝ, the following hold: 1) WA no guarantee: It is possible that VM (s) ⪯ VM̂ (ŝ) or that VM̂ (ŝ) ⪯ VM (s). 2) IMDP guarantee: WM̂ (ŝ) ⪯ VM (s) ⪯ BM̂ (ŝ). 3) SG guarantee: VĜ (ŝ) ⪯ VM (s) ⪯ BĜ (ŝ).
A. Setup Implementation. Our implementation builds on the model checkers PRISM [2] and Storm [3]. Specifically, we use version 1.11.1 of stormpy, the Python bindings of Storm for the general framework, and adapt PRISM for computing values of SGs and IMDPs. The overall experimental pipeline is run on a 2023 MacBook Pro with Apple M3 Pro Chip and 18GiB
Proof. The full proof is in Appendix B. There, for the WA abstraction, we provide concrete counterexamples where
7
Fig. 7: Performance of different causal partitions across benchmarks.
RAM. Cause computations were carried out with a fully BDDbased version of [8] based on Coudert and Madre’s implicit prime implicant algorithm [46], and run on a workstation with Debian 12 Bookworm with AMD Ryzen Threadripper PRO 5965WX 24-Cores CPU and 8x64GiB Samsung DDR4-3200 RAM. The most expensive step of feature cause calculation uses a timeout of up to 12 hours, see Appendix C-C for details. Our implementation is available on GitHub, see Appendix D.
(RQ1) How does the property affect performance?
Benchmarks. We use the MDPs collected in [47] that are available in PRISM format and have unbounded reachability or safety properties. We exclude models where Pmin =1 or Pmax =0, as well as highly synthetic verification benchmarks with low inherent meaning in their state features. We configure the benchmark parameters to state spaces in the order of 104 (small), 105 (medium), and 106 (large). A full list is in Table II.
For the C-1 partition, results are similar across hyperparameters. The detailed analysis in Appendix C-A, Table I, shows that the relative threshold with ϵ = 0.1 achieves the best policy performance across benchmarks. We deem this the most important metric for the quality of our abstraction. For Effect choices, interpretations that find causes for large parts of the state space (3 and 4 in Fig. 4) lead to the best abstractions.
Algorithms. We consider all variants of Effect and Valid sets introduced in Section IV, as well as the three partition types, namely causal graph (C-G), one-shot (C-1), and iterative (C-IT). We combine these with the three aggregation methods WA, IMDP, and SG, resulting in names such as C-IT-SG.
For the C-IT partition, we receive better abstractions with fixed numbers of iterations. Like with C-1, we find that results are very similar across thresholds, and also when using 6 or 10 fixed iterations. Fig. 12 and Fig. 13 in Appendix C-A include detailed analysis. Between fixed thresholds or numbers of iterations, we observe that fixing the number of iterations leads to slightly larger abstractions, but with highly improved interval bounds and policy performance.
The Effect set can vary depending on interpretation (see Fig. 4) and value threshold. We group the interpretations into those that capture “good” and “bad” effects. For maximizing properties, 3 and 1 capture “good” effects whereas 2 and 4 capture “bad” effects. Moreover, for the C-IT partition, we can pre-determine a desired number of iterations. We analyse configurations using the SG method on small models.
Remark 3. Our empirical evaluation focuses on reachability properties with minimizing and maximizing objectives. The former is also called safety, with the intuition that the probability of reaching a safety-critical state is minimized. Further, our definitions immediately includes reach-avoid properties, which we also analyse empirically. Extending our work to rewardbased properties would require only minor changes to definitions and proof statements, but does not affect the derivation of causes. We exclude them, however, since checking rewardbased properties on non-graph-preserving interval models is currently not supported PRISM or Storm.
We use our findings to fix hyperparameters for the subsequent experiments. Overall we find that while some hyper-parameter values have little influence, such as the concrete threshold values, others matter greatly. In particular, we find that the semantics of the Effect set are decisive, and we observe the best performance with Effect sets covering a large part of the “good” states. Based on these findings, for the C-1 partition, we continue with relative ϵ = 0.1 and use the Effect sets numbered 3 and 4 in Fig. 4. For the C-IT partition, we again observe that concrete threshold values have little impact, but fixing a larger number of iteration yields better performance. Therefore, we iterate 6 times, since that leads to the best ratio of performance and computational effort. In both cases, we observe that “good” effect sets achieve better abstractions than “bad” effects and include visualizations in the appendix in Fig. 14. To still cover both interpretations, we continue with the hyperparameters on both types of effects.
Metrics. We consider three metrics: (1) the size of the abstraction relative to the original model size, (2) the difference between the worst and best case value for the IMDP and SG aggregation method, and (3) the relative difference between the optimal policy in the MDP and the worst case abstract policy, scaled by the difference between minimal and maximal reachability probability (see Appendix C-D). All metrics range from 0 to 1, and small values are preferable.
8
Fig. 8: Comparing the performance of different abstraction methods.
Fig. 9: Generalizing causes from the small models to larger model sizes.
(RQ2) How do different causal partitions compare? We compare the C-G, C-IT, and C-1 partitions with the previously fixed hyperparameters using the SG abstraction. The C-G partition uses the same causes as C-1. The C-G partition does not modify the model in 38% of our benchmarks. In these cases, no state variables can be completely removed since all are causally relevant to the property in some states. That means the abstract and original model are the same. We exclude those benchmarks from further evaluation but include details in the appendix, Fig. 15. C-IT partitions produce better abstractions than C-1 and C-G. In terms of model size, the C-1 partition produces the smallest abstract models on most benchmarks, retaining less than 20% of the original states on 13 out of 14 benchmarks. C-G returns the largest sized abstractions on most benchmarks. However, all three partitions are able to significantly reduce model sizes across benchmarks. On the qualitative metrics however, C-IT-based abstractions achieve the smallest value bounds and best policy performance, with small bounds on 10 out of 14 benchmarks and good policies on 5 out of 14 benchmarks. These results are visualized in Fig. 7. We find that C-G, which is usually employed by related works, is consistently outperformed. C-IT performs best, as it captures
the most fine-grained interplay of causes. It is, however, expensive to derive. C-1, with lower computational cost and often reasonable performance marks a middle ground. (RQ3) How do different aggregation methods compare? We compare the performance of the aggregation methods in Fig. 8, with more details in the appendix (Figs. 16 and 17). Our empirical results confirm Theorem 2, i.e., the interval for the abstract IMDP and SG always contain the original value. SG abstractions perform best, followed by IMDP and WA. Since all abstractions are built from the same partition, abstract model size is always the same. The SG abstractions mostly achieve smaller interval value bounds than the IMDP ones, often even achieving an interval size of 0. The policy performance however differs more strongly between the abstraction methods. WA abstractions often achieve a policy difference close to 0, but can also result in arbitrarily wrong policies without any guarantees. Between IMDPs and SGs, the results are often similar. As in the previous experiments, we observe that all methods perform better on effects that are interpreted as “good” than those that are “bad” (see Appendix C-A). Our findings here show a trade-off between performance and guarantees versus computational cost. Particularly, the SG
9
aggregations offers guarantees and the best performance, as it tightly preserves uncertainty. This however comes at increased computational cost, compared to WA. The latter still often performs well and is easy to solve, but can be arbitrarily wrong, as the averaging may neglect specific behaviors.
solely dependent on a single state, do not produce effective abstractions. These benchmarks can show extreme differences in values between states, leading to a singular cause, and an abstraction consisting of only two abstract states. Regarding the practical implications to draw from our experiments, in particular, we find a trade-off between computational expenses and the informativeness of partitions and therein the preciseness of abstractions. Specifically, we find that a combination of C-IT-SG is the most reliable yet most expensive choice. C-1-WA on the other hand offers a lightweight heuristic without guarantees on abstraction quality, that nonetheless often works well in practice. However, combinations of C-1 or C-IT with the SG aggregation method is preferable when guarantees matter.
(RQ4) Do the causal partitions generalize to larger models? Using causality in MDPs and RL is often motivated by the potential of causal relations to generalize to scaled-up models. We test the potential of our causes to generalize to medium and large sized models (see Table II). We apply causes retrieved on small models to larger settings, and report the results in Fig. 9. Additionally, the appendix compares with mediumsized causes on the medium-sized models. The causes generalize well in terms of size but at reduced performance. The small causes decrease the relative size of larger models to less than 20%, even in cases where the small abstraction maintained more than 60% of the original size. However, the policy difference often becomes worse, sometimes degrading to the worst possible policy. Still, on several models, the abstract policy attains a policy difference close to 0 on the large models, indicating optimal performance.
VII. C ONCLUSION We formalize feature causality in MDPs to derive several types of property-driven predicate-based causal abstractions. We combine our causal state space partitions with three aggregation methods and analyze their theoretical (dis-)advantages. Empirical evaluation shows that our proposed methods can significantly reduce model size while maintaining good policy performance on several standard benchmarks. Further, the derived feature causes show potential to generalize to larger model sizes. A relevant limitation is that our approach requires to exactly analyze the full model to obtain the causal information. However, our aim is to gain a fundamental understanding of how causality can be applied to obtain abstractions that are capable of retaining relevant parts of the model. Future work aims to tackle this limitation by, among others, approximating the causal predicates from data or learned models.
Abstract policies perform well on large models. The policy performance for large models is often closer to the original model performance than for medium abstractions, even if both are derived from small causes. This is interesting, as obtaining causes for larger models is computationally more expensive. Our findings demonstrate the potential of our approach and provide an avenue to efficiently apply property-driven causal abstractions even on large models, provided they are parameterized to allow for small variants.
R EFERENCES
Causes fitted to the model size increase performance, but are computationally expensive. As we show in the appendix in Fig. 18 and Fig. 19, those abstractions built from mediumsized causes usually receive tighter value bounds and better policy performance. The calculation of most general causes however becomes more computationally expensive on larger models, with several experimental configurations timing out even after 12 hours, as documented in Table III. Our straightforward approach for generalizing causes between models shows our framework’s potential to scale to models of larger sizes without further increase in computational demands.
[1] A. L. Strehl, C. Diuk, and M. L. Littman, “Efficient structure learning in factored-state mdps,” in AAAI, pp. 645–650, AAAI Press, 2007. [2] M. Z. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verification of probabilistic real-time systems,” in CAV, vol. 6806 of Lecture Notes in Computer Science, pp. 585–591, Springer, 2011. [3] C. Hensel, S. Junges, J. Katoen, T. Quatmann, and M. Volk, “The probabilistic model checker storm,” Int. J. Softw. Tools Technol. Transf., vol. 24, no. 4, pp. 589–610, 2022. [4] 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. [5] T. D. Simão, N. Jansen, and M. T. J. Spaan, “Alwayssafe: Reinforcement learning without safety constraint violations during training,” in AAMAS, pp. 1226–1235, ACM, 2021. [6] J. Pearl, Causality. Cambridge University Press, 2 ed., 2009. [7] J. Y. Halpern, Actual Causality. The MIT Press, 08 2016. [8] C. Dubslaff, K. Weis, C. Baier, and S. Apel, “Feature causality,” J. Syst. Softw., vol. 209, p. 111915, 2024. [9] 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. [10] M. Kattenbelt, M. Z. Kwiatkowska, G. Norman, and D. Parker, “A gamebased abstraction-refinement framework for markov decision processes,” Formal Methods Syst. Des., vol. 36, no. 3, pp. 246–280, 2010. [11] E. Eells, Probabilistic Causality. Cambridge Studies in Probability, Induction and Decision Theory, Cambridge University Press, 1991. [12] J. Peters, D. Janzing, and B. Schölkopf, Elements of Causal Inference: Foundations and Learning Algorithms. Cambridge, MA, USA: MIT Press, 2017. [13] J. Y. Halpern, “A modification of the halpern-pearl definition of causality,” in IJCAI, pp. 3022–3033, AAAI Press, 2015.
B. General findings and practical implications In our empirical evaluation, we observe an overall mixed performance across benchmarks, and across combinations of partitions and aggregation methods. We now provide further insights on our key takeaways from this evaluation. Concerning benchmarks, we find that our abstractions are effective when whole state variables or large parts of their domain are irrelevant to the property of interest. In these cases, our abstractions become very small in size while maintaining good policy performance. On the other hand, handcrafted and highly artificial models where state variables do not carry much structural meaning, and where the outcome is
10
Proceedings of Machine Learning Research, pp. 23151–23180, PMLR, 2022. [38] Z. Wang, C. Wang, X. Xiao, Y. Zhu, and P. Stone, “Building minimal and reusable causal state abstractions for reinforcement learning,” Proceedings of the AAAI Conference on Artificial Intelligence, vol. 38, 2024. [39] S. Pranger, H. Chockler, M. Tappler, and B. Könighofer, “Test where decisions matter: Importance-driven testing for deep reinforcement learning,” in Advances in Neural Information Processing Systems (A. Globerson, L. Mackey, D. Belgrave, A. Fan, U. Paquet, J. Tomczak, and C. Zhang, eds.), vol. 37, pp. 28103–28126, Curran Associates, Inc., 2024. [40] M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics, Wiley, 1994. [41] C. Baier and J.-P. Katoen, Principles of model checking. MIT Press, 2008. [42] A. Condon, “The complexity of stochastic games,” Inf. Comput., vol. 96, no. 2, pp. 203–224, 1992. [43] J. Jackson, L. Laurenti, E. W. Frew, and M. Lahijanian, “Strategy synthesis for partially-known switched stochastic systems,” in HSCC, pp. 6:1–6:11, ACM, 2021. [44] K. Chatterjee and T. A. Henzinger, “Value iteration,” in 25 Years of Model Checking, vol. 5000 of Lecture Notes in Computer Science, pp. 107–138, Springer, 2008. [45] G. N. Iyengar, “Robust dynamic programming,” Mathematics of Operations Research, vol. 30(2), pp. 257–280, 2005. [46] O. Coudert and J. C. Madre, “Implicit and incremental computation of primes and essential primes of boolean functions,” in DAC, pp. 36–39, IEEE Computer Society Press, 1992. [47] 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.
[14] C. Dubslaff, K. Weis, C. Baier, and S. Apel, “Causality in configurable software systems,” in Proceedings of the 44th International Conference on Software Engineering (ICSE), 2022. [15] 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. [16] C. Baier, C. Dubslaff, F. Funke, S. Jantsch, R. Majumdar, J. Piribauer, and R. Ziemek, “From verification to causality-based explications,” in Proceedings of the 48th International Colloquium on Automata, Languages, and Programming (ICALP), 2021. [17] 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. [18] R. Oura and Y. Ito, “Probability-raising causality for uncertain parametric markov decision processes with PAC guarantees,” in UAI, vol. 286 of Proceedings of Machine Learning Research, pp. 3300–3321, PMLR, 2025. [19] E. Ábrahám and B. Bonakdarpour, “HyperPCTL: A temporal logic for probabilistic hyperproperties,” in Proc. of the 15th Intern. Conf. on Quantitative Evaluation of Systems (QEST), pp. 20–35, Springer, 2018. [20] R. Dimitrova, B. Finkbeiner, and H. Torfah, “Probabilistic Hyperproperties of Markov Decision Processes,” in Proc. of the 18th Intern. Symp. on Automated Technology for Verification and Analysis (ATVA), vol. 12302 of LNCS, pp. 484–500, Springer, 2020. [21] M. Kazemi, J. Lally, and N. Paoletti, “Causal temporal reasoning for markov decision processes,” Research Directions: Cyber-Physical Systems, vol. 3, p. e3, 2025. [22] 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. [23] Y. Zeng, R. Cai, F. Sun, L. Huang, and Z. Hao, “A survey on causal reinforcement learning,” CoRR, vol. abs/2302.05209, 2023. [24] Z. Deng, J. Jiang, G. Long, and C. Zhang, “Causal reinforcement learning: A survey,” 2023. [25] E. Bareinboim, A. Forney, and J. Pearl, “Bandits with unobserved confounders: A causal approach,” in NIPS, pp. 1342–1350, 2015. [26] A. Méndez-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. [27] H. Sun, “Toward causal-aware RL: state-wise action-refined temporal difference,” CoRR, vol. abs/2201.00354, 2022. [28] M. Gasse, D. Grasset, G. Gaudron, and P. Oudeyer, “Causal reinforcement learning using observational and interventional data,” CoRR, vol. abs/2106.14421, 2021. [29] L. Li, T. J. Walsh, and M. L. Littman, “Towards a unified theory of state abstraction for MDPs,” in AI&M, 2006. [30] K. G. Larsen and A. Skou, “Bisimulation through probabilistic testing,” Information and Computation, vol. 94, no. 1, pp. 1–28, 1991. [31] 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. [32] N. Ferns, P. Panangaden, and D. Precup, “Metrics for finite markov decision processes,” in Proceedings of the 20th Conference on Uncertainty in Artificial Intelligence, UAI ’04, (Arlington, Virginia, USA), pp. 162– 169, AUAI Press, 2004. [33] S. S. Ruan, G. Comanici, P. Panangaden, and D. Precup, “Representation discovery for mdps using bisimulation metrics,” in Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI’15, pp. 3578–3584, AAAI Press, 2015. [34] K. Batz, S. Junges, B. L. Kaminski, J.-P. Katoen, C. Matheja, and P. Schröer, “Pric3: Property directed reachability for mdps,” in Computer Aided Verification (S. K. Lahiri and C. Wang, eds.), (Cham), pp. 512– 538, Springer International Publishing, 2020. [35] J. Lally, M. Kazemi, and N. Paoletti, “Robust counterfactual inference in markov decision processes,” 2026. accepted for publication at AAMAS 2026. [36] A. Zhang, C. Lyle, S. Sodhani, A. Filos, M. Kwiatkowska, J. Pineau, Y. Gal, and D. Precup, “Invariant causal prediction for block mdps,” in ICML, vol. 119 of Proceedings of Machine Learning Research, pp. 11214–11224, PMLR, 2020. [37] Z. Wang, X. Xiao, Z. Xu, Y. Zhu, and P. Stone, “Causal dynamics learning for task-independent state abstraction,” in ICML, vol. 162 of
11
A PPENDIX A P ROOFS FOR S ECTION IV
Proof outline. We need to show four inequalities. The proof is done as follows. 1) 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. 2) Then, we show that these interval distributions belong to MDPs consistent with the IMDP in Lemma 2. 3) 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 for opt = max, W(ŝ) ≤ V(s) and point out the differences where applicable for the three remaining cases.
A. Proof of Theorem 1 Intuitively, Theorem 1 claims that for a given MDP M with Valid, Effect, and a cause-effect cover C, the cardinality of PredPart(M, C) is always smaller than or equal to the cardinality of CGPart(M, Iirr ). Proof. The second claim follows from the first. Formally, the set of irrelevant features is Iirr = {i : ∄γ ∈ C : fi,k ⊂ γ, k ∈ [0..|Xi |] | i ∈ [1..n]} 1) Let i ∈ Iirr be the index of an irrelevant feature. Then, by definition, fi,k ̸⊂ γ, k ∈ [1..|Xi |, γ ∈ C]. Otherwise, it would violate Definition 4, Item (C2). Let SCG ∈ CGPart(M, Iirr ). By definition, ∀s, s ′ ∈ SCG , the states only differ in irrelevant features, i.e., ∀i ∈ [1..n]\Iirr : xi′ = xi . Hence, γ(s) = γ(s ′ ) forall γ ∈ C, i.e., s, s ′ are in the same SP ∈ PredPart(M, C). Therefore, the first claim holds. 2) If for all sets SCG there is a set SP such that SCG = SP , then |CGPart(M, Iirr )| = |PredPart(M, C)|. If some SP ∈ PredPart(M, C) is a superset of multiple SCG ∈ CGPart(M, Iirr ), then |CGPart(M, Iirr )| > |PredPart(M, C)|.
Necessary lemmas and their proofs. Lemma 1. There exist interval policies π2 such that the induced probability distributions give valid upper and lower bounds on the values of the original MDP. In all cases, we show the bounds ∀ŝ ∈ Ŝ, ∀a ∈ A where a = π(s) = π̂(ŝ)∀s ∈ S, as described in Section V-B. Lower bound. For opt = max, W(ŝ) ≤ V(s) and for opt = min, B(ŝ) ≤ V(s). Let f : Ŝ → [0, 1]. Then: X XX P̂ π2 (q̂) · f (q̂) ≤ min P(q ′ ) · f (q̂). min P̂ π2 ∈U (ŝ,a)
s∈ŝ
q̂∈Ŝ
′
q̂∈Ŝ q ∈q̂
I.e., the value of the probability distribution P̂ π2 with the smallest value in M̂ is smaller or equal to the value of the state s ∈ ŝ with smallest value in M.
A PPENDIX B P ROOFS FOR S ECTION V
Upper bound. For opt = max, B(ŝ) ≥ V(s) and for opt = min, W(ŝ) ≥ V(s). Let f : Ŝ → [0, 1]. Then: XX X P(q ′ ) · f (q̂). P̂ π2 (q̂) · f (q̂) ≥ max max
A. Proof of Theorem 2 - Item 1 We show that the WA abstraction can lead to arbitrarily wrong values using the counter-examples in Fig. 10. In the MDP M, the maximum probability to reach s2 is 0.6, by first playing a and then b. Grouping together the states {s0 , s1 }, we obtain the abstract MDP M̂1 . There, the maximum probability to reach s2 is 1/2 (by playing b), strictly smaller than in the original MDP. Grouping together the states {s0 , s1 , s3 }, we obtain the abstract MDP M̂2 . There, the maximum probability to eventually reach s2 is 1 (by forever playing b), strictly larger than in the original MDP.
P̂ π2 ∈U (ŝ,a)
s∈ŝ
q̂∈Ŝ
′
q̂∈Ŝ q ∈q̂
I.e., the value of the probability distribution P̂ π2 with the largest value in M̂ is larger or equal to the value of the state s ∈ ŝ with largest value in M. Proof. Let ŝ ∈ Ŝ an abstract state in M̂. Let n = |Ŝ|. We define an ordering of abstract successor states of ŝ. For lower bounds, let q̂1 , . . . , q̂n be an ordering over abstract successor states of ŝ where ∀i ∈ [1..n) : f (q̂i ) ≤ f (q̂i+1 ). I.e., the successors are ordered by value in ascending order. Analogously for upper bounds, let q̂1 , . . . q̂n be an ordering over the abstract successors of ŝ where ∀i ∈ [1, n) : f (q̂i ) ≥ f (q̂i+1 ), i.e., ordered by value in descending order. InP both cases, j is the index of the state in the P ordering such j that i=1 P̂U (q̂i ) > 1 − Base, with Base = q̂∈Ŝ P̂L (q̂). Then, P̂ π2 is a fixed probability distribution, such that for all ordered successor states q̂i ,
B. Proof of Theorem 2 - Item 2 Notes on notation. For a given IMDP M̂, we write π2 to refer to the choice of probability distribution, or choice of consistent MDP, from the set of MDPs consistent with M̂. Further, we write P̂ π2 for the probability distribution induced by an interval policy π2 . We call U (ŝ, a) the uncertainty set, i.e., the set of possible probability distributions given an abstract state ŝ and action a. The uncertainty set of the IMDP contains all the MDPs consistent with the IMDP. For ease of notation, we introduce the following shorthands: ′ ′ • P(q ) = P(s, a, q ) π2 π2 • P̂ (q̂) = P̂ (ŝ, a, q̂) • P̂L (q̂i ) = P̂L (ŝ, a, q̂i ) • P̂U (q̂i ) = P̂U (ŝ, a, q̂i )
i<j P̂U (q̂i ) π2 P̂ (q̂i ) = P̂L (q̂i ) i>j. Pj−1 Pn 1 − i=1 P̂U (q̂i ) − i=j+1 P̂L (q̂i ) i = j Lemma 2 shows that P̂ π2 is a valid distribution.
12
a, b
a a
s0
0.6
b
s1
s2 a
0.4
{s2 }
a, b
a
0.5
b
{s0 , s1 }
s3
b a
0.8
a, b
{s3 }
0.2
a, b
1/3
2/3
(b) Abstract MDP M̂1 , grouping {s0 , s1 }.
(a) Original MDP M.
b
{s0 , s1 , s3 }
0.5
{s2 } a, b
(c) Abstract MDP M̂2 , grouping {s0 , s1 , s3 }.
Fig. 10: MDPs and their WA abstractions to show Item 1 of Theorem 2.
We now show the claim of Lemma 1. We include the full proof for the lower bound opt = max, W(ŝ) ≤ V(s), which is identical to opt = min, B(ŝ) ≤ V(s). For upper bounds, we replace every mins∈ŝ with maxs∈ŝ and every ≤ with ≥.
=
j−1 X
X
min s∈ŝ
i=1
q ′ ∈q̂i
j−1 X
+ (1 − j−1 X
P̂U (q̂i ) −
s∈ŝ
i=1
≤
j−1 X
s∈ŝ
s∈ŝ
P̂U (q̂i )
i=1
P(q ′ )) · f (q̂j )
X
n X
P(q ′ ) · f (q̂i ) +
q ′ ∈q̂i
X
+ (min
j−1 X
P̂L (q̂i ) +
q ′ ∈q̂i
min
i=1
n X i=j+1
X
min
P̂L (q̂i ) · f (q̂i )
i=j+1
i=1
−
n X
P(q ′ ) · f (q̂i ) +
P̂L (q̂i a) · f (q̂i )
i=j+1
P(q ′ ) +
q ′ ∈q̂j
n X
(P̂L (q̂i ) − min s∈ŝ
i=j+1
X
P(q ′ ))) · f (q̂j )
q ′ ∈q̂i
(Remark 4) X
≤
P̂ π2 (ŝ, a, q̂) · f (q̂)
=
P̂U (q̂i ) · f (q̂i ) +
+ (1 −
j−1 X
P̂U (q̂i ) −
i=1
=
j−1 X i=1
+
P̂L (q̂i ) · f (q̂i )
n X
+
P̂L (q̂i )) · f (q̂j )
X
=
P(q ′ ) + P̂U (q̂i ) − min s∈ŝ
q ′ ∈q̂
P̂L (q̂i ) · f (q̂i ) + (1 −
j−1 X
i=j+1
≤
j−1 X
min s∈ŝ
i=1
X
− min s∈ŝ
X
′
P(q ) · f (q̂i ) +
q ′ ∈q̂
P(q ′ )) · f (q̂j ) +
j−1 X i=1
P(q ′ )) · f (q̂i )
P̂U (q̂i ) −
j−1 X
P̂L (q̂i )) · f (q̂j ) = i=j+1
n X
j X
(P̂U (q̂i )
=
i=1 n X
P̂L (q̂i ) · f (q̂i )
(Remark 5)
q ′ ∈q̂i n X
P(q ′ ) · f (q̂i ) +
q ′ ∈q̂i
(P̂L (q̂i )
i=j+1
P(q ′ ) − P̂L (q̂i )) · f (q̂i )
min s∈ŝ
min s∈ŝ
X q ′ ∈q̂
q ′ ∈q̂
≤ min
XX
n X
P(q ′ ) · f (q̂i ) +
i=j+1
i
X
q̂∈Ŝ s∈ŝ
P(q ′ ) − P̂L (q̂i )) · f (q̂i )
q ′ ∈q̂i
i=1
X
X
X
X
s∈ŝ
i=j+1
P̂U (q̂i ) −
s∈ŝ
+ min
n X
s∈ŝ
min
i=1
q ′ ∈q̂
i=1
q ′ ∈q̂
+ (1 −
X
(min
j X
P̂L (q̂i ) · f (q̂i )
i=j+1
P(q ′ ) · f (q̂j )
q ′ ∈q̂j n X
i=j+1
i=j+1
(min s∈ŝ
n X
X
n X
P(q ′ ) · f (q̂i ) +
q ′ ∈q̂i
s∈ŝ
i=j+1
i=1
s∈ŝ
+ min
n X
X
min
i=1
q̂∈Ŝ j−1 X
j−1 X
min s∈ŝ
X q ′ ∈q̂
P(q ′ ) · f (q̂i )
i
′
P(q ) · f (q̂) P(s, a, q ′ ) · f (q̂)
′
q̂∈Ŝ q ∈q̂
Since we can show the inequality and since minP̂ π2 ∈U ≤ P̂ π2 because P̂ π2 ∈ U, the claim holds for lower bounds.
P̂L (q̂i )) · f (q̂j )
i=j+1
(Note: f (q̂i ) ≤ f (q̂j )∀i < j) Remark 4. For lower bounds, we need to show that
13
Remark 5. For lower bounds, we show that:
1−
j−1 X
P̂U (q̂i ) −
i=1
+
j−1 X
n X
n X
P̂L (q̂i )
i=j+1 n X
i=j+1
≤
X
(P̂U (q̂i ) − min s∈ŝ
i=1
≤ min
X
s∈ŝ
q ′ q̂
P(q ′ ) +
′
P(q ))
(P̂L (q̂i ) − min s∈S
i=j+1
j
X
P̂U (q̂i ) −
i=1
+
j−1 X
n X
P(q ′ ))
≤
P̂L (q̂i )
(P̂U (q̂i ) − min s∈ŝ
s∈ŝ
X
′
P(q ) +
q ′ q̂j n X
s∈ŝ
P(q ′ ) +
s∈ŝ
s∈S
X q ′ q̂
X
min
P(q ′ )) +
q ′ ∈q̂i n X
min
n X
(min s∈ŝ
n X
P(q ))
n X
n X
X
′
P(q ′ ) − P̂L (q̂i )) · f (q̂i )
P(q ) ≤ X
X
i=j+1
s∈S
q ′ ∈q̂i
n X
q ′ ∈q̂i
X
min s∈ŝ
n X
P(q ′ ) · f (q̂i ) −
q ′ ∈q̂
P(q ′ ) · f (q̂j )
i
P̂L (q̂i ) · f (q̂i )
i=j+1
P̂L (q̂i ) · (f (q̂j ) + f (q̂i ))
P(q ′ ))
n X
min
i=j+1
q ′ ∈q̂i
⇐⇒
s∈ŝ
n X
X
P(q ′ ) · (f (q̂i ) + f (q̂j )
q ′ ∈q̂i
P̂L (q̂i ) ≤
P̂L (q̂i )
n X i=j+1
i=j+1
s∈S
X
min s∈ŝ
min s∈ŝ
X
P(q ′ ) (Definition 6)
q ′ ∈q̂i
Lemma 2. The interval distribution for lower bounds fixed in Lemma 1 belongs to an MDP consistent with M̂, i.e., P̂ π2 ∈ U, where π2 is the lower bound interval distribution. The same holds for upper bounds, i.e., P̂ π2 ∈ U, where π2 is the upper bound interval distribution.
P(q ′ )
q ′ ∈q̂i
P(q ′ ))
min s∈ŝ
X
X
Proof. The interval distribution is chosen identically for both upper and lower bounds, differing only in the direction of ordering over abstract successor states. It is therefore sufficient to show the validity of the interval distribution P̂ π2 once. We need to show that ∀(ŝ, a), P̂ π2 (1) is a valid probability distribution, and (2) lies within the interval bounds for each successor state q̂ ∈ Ŝ. 1) ∀ŝ, a ∈ Ŝ × A, P̂ π2 is a valid probability distribution:
P(q ′ )
q ′ ∈q̂i
P(q ′ ))
q ′ ∈q̂i
P̂U (q̂i ) +
i=1
min
i
q ′ ∈q̂i
j−1 X
⇐⇒
P(q ′ )) · f (q̂j )
i=j+1
P̂L (q̂i ) + 1
X
q ′ ∈q̂
i=j+1
s∈ŝ
n X
⇐⇒
i=j+1
n X
X
P̂L (q̂i ) · f (q̂j ) −
min
i=j+1
q ′ ∈q̂i
n X
min
i=j+1
≤2·
s∈S
X
i=1
i=j+1
n X
j−1 X i=1
P̂L (q̂i ) +
⇐⇒ 1 + 2 ·
P(q ′ ) − P̂L (q̂i )) · f (q̂i )
q ′ ∈q̂i
i=j+1
i=j+1
≤2·
′
q ′ ∈q̂i
s∈S
P(q ′ ) + 2 ·
X q ′ ∈q̂i
(P̂L (q̂i ) − min
j
⇐⇒ 1 + 2 · n X
s∈ŝi
i=j+1
⇐⇒ 1 ≤ min
i=j+1
n X
X
min
i=1
q ′ q̂j
n X
≤ s∈S
P̂L (q̂i ) −
q ′ ∈q̂i
i=j+1
(P̂L (q̂i ) − min
i=j+1
≤ min
P(q ))
q ′ ∈q̂i n X
i=j+1
⇐⇒ 1 − X
′
j−1 X
s∈ŝ
i=j+1
⇐⇒
≤ min
−
(P̂L (q̂i ) − min
i=j+1
i=1
s∈ŝ
X
P(q ′ )) · f (q̂j )
That is done by solving the following inequality:
i=j+1 n X
X
(min
X
q ′ ∈q̂i
This is done as follows: j−1 X
s∈ŝ
i=j+1
q ′ ∈q̂i n X
n X
1−
(P̂L (q̂i ) − min
P(q ′ )) ≤
n X
j−1 X
P̂L (q̂i ) (Definition 6)
i=1
i=j+1
n X
P̂L (q̂i ) + 1−
i=j+1
P̂U (q̂i ) −
n X
P̂L (q̂i ) = 1
i=j+1
2) ∀ŝ, a ∈ Ŝ × A, P̂ π2 is within the valid interval bounds. • For i < j and i > j, this follows from Definition 6 which explicitly includes the interval bounds, and
14
W≤k+1 (ŝ) = max
P̂ π2 (q̂i ) = P̂U (q̂i ) and P̂ π2 (q̂i ) = P̂L (q̂i ). •
a∈A P̂ π2 ∈U (ŝ,a)
For i = j, we show that P̂L (q̂j ) ≤ P̂ π2 (q̂j ) ≤ P̂U (q̂j ). Pj For the upper bound, since k=1 P̂U (q̂k ) > 1 − Base Pj−1 but by construction, k=1 P̂U (q̂k ) ≤ 1 − Base, we have that P̂U (q̂j ) ≥ P̂ π2 (q̂j ).
P̂L (q̂j ) > 1 −
P̂U (q̂i ) −
i=1
=⇒ P̂L (q̂j ) + P̂L (q̂j ) +
n X
≤ max
X
a∈A
(min s∈ŝ
+
q̂∈Ŝ
X
P(q ′ )) · W≤k (q̂)
q̂∈Ŝ
q ′ ∈q̂
≤ min max
XX
(Lemma 1) s∈ŝ a∈A
≤ min max s∈ŝ a∈A
P̂L (q̂i )
′
P(q ) · W
≤k
(q̂)
′
q̂∈Ŝ q ∈q̂
XX
P(q ′ ) · min V≤k (q ′′ ) ′′ q ∈q̂
′
q̂∈Ŝ q ∈q̂
(Induction hypothesis)
i=j+1 j−1 X
≤ min max
P̂U (q̂i )
XX
s∈ŝ a∈A
i=1 n X
P̂ π2 (q̂) · W≤k (q̂) (k-step VI [44])
We prove the lower bound by contradiction. Assume P̂L (q̂j ) > P̂ π2 (q̂j ). Then, j−1 X
X
min
= min max
q̂∈Ŝ
X
P(q ′ ) · V≤k (q ′ )
s∈ŝ a∈A
P̂L (q̂i ) > j
i=j+1
= min V s∈ŝ
P(q ′ ) · V≤k (q ′ ) (Remark 6)
q ′ ∈q̂
q ′ ∈S ≤k+1
(s)
(Remark 7) (k-step VI [44])
For the best case lower bound where opt = min, B(ŝ) ≤ V(s), we replace all occurrences of maxa∈A with mina∈A and W(ŝ) with B(ŝ) in the induction. For the remaining cases, the abstract target set definition changes to T̂ = { ŝ | ∃s ∈ T ∧ ŝ}. That changes the base case of induction as follows: If ŝ ∈ T̂, then ∃s ∈ ŝ : s ∈ T. Therefore, ∃s ∈ ŝ : W≤0 (ŝ) = 1 = V≤0 (s). Then, for the worst case upper bound where opt = min, W(ŝ) ≤ V(s), we replace all occurrences of min with max and conversely all occurrences of max with min and exchange all occurrences of ≤ with ≥. Finally, for the best case upper bound where opt = min, B(ŝ) ≥ V(s), we replace all minP̂ π2 ∈U with maxP̂ π2 ∈U , and change all occurrences of ≤ with ≥. Thus, by convergence of value iteration [44], ∀ŝ ∈ Ŝ : opt = max :
This cannot hold since previously showed that P π2 π2 q̂∈Ŝ P̂ (q̂) = 1. Hence, P̂L (q̂j ) ≤ P̂ (q̂j ).
Overall proof of Theorem 2 - Item 2. Using the results from the above steps, we prove the inequalities of Theorem 2 - Item 2 by induction.
Proof. The proof is fully analogous in all four cases. Therefore, we provide the full proof for opt = max, W(ŝ) ≤ V(s), i.e., the worst case lower bound and point out differences for the remaining cases.
W(ŝ) = lim W≤ (ŝ) ≤ lim min V≤k (s) = min V(s)
We show by induction that
k→∞ s∈S
k→∞
s∈ŝ
≤
B(ŝ) = lim B (ŝ) ≥ lim max V k→∞ s∈S
k→∞
∀k ∈ N0 .W≤k (ŝ) ≤ min V≤k (s), ∀ŝ ∈ Ŝ, s ∈ ŝ
≤k
(s) = max V(s) s∈ŝ
opt = min :
s∈ŝ
W(ŝ) = lim W≤ (ŝ) ≤ lim max V≤k (s) = max V(s) k→∞ s∈S
k→∞
≤
s∈ŝ
B(ŝ) = lim B (ŝ) ≤ lim min V
Base case. If ŝ ∈ T̂, then s ∈ T∀s ∈ ŝ. Therefore
k→∞ s∈S
k→∞
∀s ∈ ŝ, W≤0 (ŝ) = 1 = V≤0 (s)
≤k
(s) = min V(s) s∈ŝ
Remarks supporting the induction. The following remarks extend on the referenced induction steps in the proof of Theorem 2 - Item 2. Remark 6. Let opt ∈ {min, max}. For the lower bound, we have XX min opta∈A P(q ′ ) · min V≤k (q ′′ ) ′′
Induction hypothesis.
∀ŝ ∈ Ŝ, ∀k ∈ N0 : W≤k (ŝ) ≤ min V≤k (s)
s∈ŝ
≤ min opta∈A
XX
s∈ŝ
q̂∈Ŝ
Induction step. ∀ŝ ∈ Ŝ :
15
q ∈q̂
′
q̂∈Ŝ q ∈q̂
s∈ŝ
q ′ ∈q̂
P(q ′ ) · V≤k (q ′ )
since min V
q ′′ ∈q̂
≤k
′′
(q ) ≤ V
≤k
′
′
(q ), ∀q ∈ q̂.
best size best interval size best policy difference size < 0.5 size < 0.3 interval size < 0.5 interval size < 0.3 policy difference < 0.5 policy difference < 0.3
Analogously, for the upper bound, we have XX max opta∈A P(q ′ ) · max V≤k (q ′′ ) ′′ s∈ŝ
q ∈q̂
′
q̂∈Ŝ q ∈q̂
≥ max opta∈A s∈ŝ
XX
P(q ′ ) · V≤k (q ′ )
percentile 0.1 0.25 64 62 23 82 98 93 95 95 85 82 29 25 25 24 34 35 27 27
relative 0.1 0.4 47 51 14 158 95 88 89 88 84 83 42 39 37 34 43 39 35 31
′
q̂∈Ŝ q ∈q̂
TABLE I: Performance of thresholds for the C-1 partition.
since max V≤k (q ′′ ) ≥ V ≤k (q ′ ), ∀q ′ ∈ q̂. ′′ q ∈q̂
S
in terms of quality. While the relative τ = 0.4 threshold often achieves the smallest interval bounds, for the fuzzy values, the relative τ = 0.1 threshold performs slightly better. Further, we do not find observe significant differences in terms of threshold performance under different combinations of ValidEffect definitions, which we visualize in Fig. 11. Overall, the differences between threshold performances are relatively small. We conclude that a relative threshold τ = 0.1 is the best threshold and use it in all further experiments. C-IT partition. We analyse the same threshold settings as previously and additionally compare this to thresholds derived from fixing a number of iterations beforehand. As we observe in Fig. 12, the results for all three metrics are very similar for different thresholds and when fixing either 6 or 10 iterations. We do, however, observe clear differences between setting thresholds and fixing the iterations in Fig. 13. Partitions from a fixed number of iterations perform better than or equal to the threshold-based iterations in terms of policy difference and tightness of value bounds. This occasionally comes at the price of larger partition cardinality. For many benchmarks, however, the size is similar or equal between the two types of iterations. Threshold-based iterations generally iterate fewer times, leading to results that are similar to the C-1 partition. Semantically interpreting Effect sets. For both partitions, we observe slightly better performance on “good” compared to “bad” Effect sets. A reason for that could be that what we interpret to be “good” effects is what the MDP benchmarks were designed for. (RQ2) How do different causal partitions compare?: In 38% of our benchmarks, the C-G partition does not exclude any features, leaving the original model untouched. For fair comparison (since policy performance and value bounds receive a perfect score of 0, since the original model is exactly reproduced), we excluded those benchmarks from the analysis in Section VI; for completeness, we include them in Fig. 15. (RQ3) How do different aggregation methods compare?: Extending: The SG aggregation works best, then IMDP, then WA. Fig. 16 shows that the SG aggregation receives small intervals on more benchmarks than the IMDP one. Whereas the IMDP models receive interval bounds of size 1 on approximatively half the benchmarks, the SG can improve bound tightness in ca. two thirds of our experiments. In terms of policy performance, all three types of models perform well on most benchmarks, with slightly better results for the SG
′
Remark 7. Since q̂∈Ŝ q ∈ q̂ = S by definition, the following holds for all four combinations of opt ∈ {min, max} and opt′ ∈ {min, max}. XX opts∈ŝ opt′a∈A P(q ′ ) · V≤k (q ′ ) ′
q̂∈Ŝ q ∈q̂
= opts∈ŝ opt′a∈A
X
P(q ′ ) · V≤k (q ′ )
q ′ ∈S
C. Proof of Theorem 2 - Item 3 Proof. Given an MDP M and a partition of its state space P . Let Ĝ be the abstract stochastic game obtained from M and P by applying Definition 7 and let Ĝ ′ be the abstract stochastic game obtained from M and P by applying [10, Definition 10]. Correctness of value bounds is proved in [10, Definition 10] for Ĝ ′ . The definition of Ĝ is identical in terms of reachability, only adding action labels for the purpose of policy generation. Transition probabilities, and therefore reachability values of the games, are computed identically. The notational differences translate as follows: • Abstract states are elements of P , called player 1 vertices in [10] and opponent states in Definition 7. In these states, policies choose a concrete lifted distribution. • Agent states (player 2 states in [10]) contain lifted distributions labeled with actions (PP in Definition 7) or ¯ in [10]). rewards (Steps • Lifted distributions are defined idenically (d in Definition 7, µ̄ in [10]). It follows that the results of [10, Theorem 1] w.r.t reachability objectives also hold for G. A PPENDIX C A DDITIONAL D ETAILS ON E XPERIMENTS A. Additional Evaluation of Experiments (RQ1) How does the property used to generate the effect set affect performance?: This section includes further evaluation details on the Effect configurations for the causal partitions. C-1 partition. We evaluate different thresholds for the C-1 partition, by counting the number of best results per threshold compared to other threshold, and use fuzzy values to count how often thresholds actually perform well. Table I shows that percentile-based thresholds often lead to partitions of smaller cardinality, but perform worse than relative thresholds
16
Fig. 13: Comparing the best performing threshold-based iteration with the best fixed number of iterations.
Fig. 11: Performance of different thresholds for the C-1 partition for different Effect-Valid configurations. Fig. 14: Good vs bad effect sets for C-IT and C-1.
Comparing performance of different partitions on “good” vs. “bad” Effect sets. Here, we find differences, especially with respect to policy quality. Across all abstraction models, “good” Effect sets usually result in larger abstract models. While the tightness of value bounds shows mixed results, there is a visible tendency towards smaller bounds on “good” effects. The distinction is clearer for policy performance, where the performance is either the same or better for “good” effects, with occasional outliers. We show this in Fig. 17. (RQ4) Do the causal partitions generalize to larger model sizes?: Fig. 18 compares the performance of small abstractions from small causes with medium abstractions from small and medium sized causes. While medium abstractions from small causes lead to relatively smaller abstractions, those from medium causes still reduce the relative size of states more than small abstractions. The interval bound tightness is often worse on medium abstractions than on small abstractions. For policy quality, the performance of medium abstractions from medium causes is usually better than for small abstractions and also compared to medium abstractions from small models. Fig. 19 directly compares the performance between medium abstractions from small and medium causes. While those abstractions from medium causes are often relatively larger than those from small causes, they often receive much tighter
Fig. 12: Performance of different iteration types for C-IT.
aggregation method. Interestingly, the WA abstraction, which does not provide guarantees on the performance of the abstract model, also receives near perfect policies for almost half the experiments, and reasonable performance in ca. 35 out of 44 benchmarks. It can however, also be arbitrarily wrong. While not interesting in settings where guarantees are required, it can still be an interesting approach for example in reinforcement learning applications due to its simplicity.
17
Fig. 15: Comparison of partitions, including benchmarks where the causal graph retains the original model.
Fig. 18: Generalization of causal abstractions. Comparing the performance of small abstractions with medium abstractions based on small or medium sized causes.
Fig. 19: Generalization of causal abstractions. Comparing the performance of medium abstractions based on small or medium sized causes.
Fig. 16: Comparison of the performance of different abstraction methods across benchmarks.
C. Feature causality time-outs We introduced timeouts for feature cause calculations. The initial timeout is 4h and then 12h. We report the settings that timed out after 4h but completed within 12h, and those that timed out even after 12h in Table III. D. Metrics For all experiments we report three performance metrics, formally defined below. We write s0 for the initial state given by the property (since all properties in our evaluation specify a unique initial state), and ŝ0 is the corresponding abstract state. Further, we write Pmax for the maximum reachability probability, i.e., maxπ∈Π Pπs0 ,M [♢T], and dually Pmin . For policy performance, by normalizing the difference with Pmax − Pmin , we achieve a relative measure of performance: If, e.g., the optimal value in the original MDP is close to 0, even a policy achieving 0 has a small absolute difference.
Fig. 17: Comparison of the performance of different abstraction methods on “good” vs. “bad” Effect sets
interval bounds and better policy quality. B. Full overview of benchmarks We include a list of benchmarks in Table II.
18
Consequently, a policy difference of 0 indicates optimal performance (Vπ (s0 ) = Vπ̂ (s0 )), while a policy difference of 1 indicates π̂ performs as bad as the worst possible policy, i.e., Vπ̂ (s0 ) = optπ∈Π Pπs,M [♢T]. relative size = |Ŝ|/|S| value bound = |W(ŝ0 ) − B(ŝ0 )| policy difference = |Vπ (s0 ) − Vπ̂ (s0 )|/(Pmax − Pmin ) A PPENDIX D A RTIFACT Code for this paper is publicly accessible on GitHub at https://github.com/ai-fm/causalabstractions.git.
19
Name avoid-mdp
consensus
consensus
csma
evade-mdp
firewire dl
mer
random-grid
refuel-mdp
sensor
zeroconf
zeroconf
Parameters N=10,slippery=0.2 N=12,slippery=0.2 N=15,slippery=0.2 N=4,K=0 N=4,K=2 N=4,K=10 N=4,K=0 N=4,K=2 N=4,K=10 N=2,K=2 N=2,K=3 N=2,K=4 N=4,slippery=0.7 N=6,slippery=0.7 N=8,slippery=0.7 delay=3,deadline=100 delay=3,deadline=200 delay=3,deadline=500 n=1,x=0.1 n=10,x=0.1 n=100,x=0.1 N=20,pover=0.3,pstay=0.3 N=40,pover=0.3,pstay=0.3 N=80,pover=0.3,pstay=0.3 N=10,ENERGY=40 N=40,ENERGY=40 N=80,ENERGY=40 N=2 N=3 N=4 N=1000,K=1,reset=false N=1000,K=2,reset=false N=1000,K=4,reset=false N=1000,K=1,reset=false N=1000,K=2,reset=false N=1000,K=4,reset=false
Property Pmax=? [”notbad” U ”goal”]
Pmin=? [F ”finished”&”all coins equal 1”]
Pmax=? [F ”finished”&!”agree”]
Pmax=? [!”collision max backoff” U ”all delivered”]
Pmax=? [”notbad” U ”goal”]
Pmin=? [F ”done”]
Pmax=? [F ”err G”]
Pmax=? [”first condition” U ”second condition”]
Pmax=? [F ”goal”]
Pmax=? [F ”condition”]
Pmax=? [F ”correct”]
Pmin=? [F ”correct”]
States 46781 84673 272701 2504 22656 43136 2504 22656 43136 1038 36850 761962 4463 63899 398271 3662 14824 113869 4356 24282 223542 7980 63960 5111920 3856 52506 161070 7222 66051 462056 31402 88858 306585 31402 88858 306585
Transitions 415105 368825 1350803 8556 75232 144352 8556 75232 144352 1282 55862 1327068 41567 698635 4601231 4898 17607 133522 17201 95069 873749 124363 1071943 8892703 24769 394218 619178 23786 263526 2156716 70643 203550 703189 70643 203550 703189
Type of model grid world
communication protocol
communication protocol
network protocol
grid world
internet protocol
resource scheduler
grid world
grid world
network protocol
internet protocol
internet protocol
TABLE II: Full overview of benchmarks. Note that configurations of avoid-mdp with N < 10 do not achieve Pmax>0, hence we cannot use them. Therefore, the smallest avoid-mdp configuration has more than > 104 states. Zeroconf with reset=false does not allow for parameter settings that result in < 105 states. Therefore we also use a larger model as the smallest here.
20
zeroconf-Pmin (m)
zeroconf-Pmax (m)
sensor (m)
sensor (s)
refuel-mdp (m)
mer (m)
mer (s)
firewire dl (m)
evade-mdp (m)
consensus-Pmin (m)
consensus-Pmin (s)
consensus-Pmax (m)
avoid-mdp (m)
avoid-mdp (s) C-1-PERC-0.1-v0e2 C-1-PERC-0.1-v0e3 C-1-PERC-0.1-v0e4 C-1-PERC-0.1-v1e1 C-1-PERC-0.1-v1e2 C-1-PERC-0.1-v2e2 C-1-PERC-0.25-v0e0 C-1-PERC-0.25-v0e1 C-1-PERC-0.25-v0e2 C-1-PERC-0.25-v0e3 C-1-PERC-0.25-v0e4 C-1-PERC-0.25-v1e1 C-1-PERC-0.25-v1e2 C-1-PERC-0.25-v2e0 C-1-PERC-0.25-v2e2 C-1-REL-0.1-v0e0 C-1-REL-0.1-v0e1 C-1-REL-0.1-v0e2 C-1-REL-0.1-v0e3 C-1-REL-0.1-v0e4 C-1-REL-0.1-v1e1 C-1-REL-0.1-v2e0 C-1-REL-0.1-v2e2 C-1-REL-0.4-v0e0 C-1-REL-0.4-v0e1 C-1-REL-0.4-v0e2 C-1-REL-0.4-v0e3 C-1-REL-0.4-v0e4 C-1-REL-0.4-v1e1 C-1-REL-0.4-v2e0 C-1-REL-0.4-v2e2 C-IT-from0-iter-6 C-IT-from0-iter-10 C-IT-from1-iter-6 C-IT-from1-iter-10 C-IT-from0-PERC-0.1 C-IT-from0-PERC-0.25 C-IT-from0-REL-0.1 C-IT-from0-REL-0.4 C-IT-from1-PERC-0.1 C-IT-from1-PERC-0.25 C-IT-from1-REL-0.1 C-IT-from1-REL-0.4
TABLE III: Timeouts when running feature causality. Cells colored green finished between 4-12 hours. Cells colored blue did not finish within 12 hours. Configurations and benchmarks without any timeouts are not included in the table.
21