Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Foundations of probability-raising causality in Markov decision processes

Christel Baier, Jakob Piribauer, Robin Ziemek

TL;DR

This paper develops a formal probabilistic causality framework for Markov decision processes by introducing probability-raising causes (SPR and GPR) under temporal priority constraints. It provides rigorous definitions, model-transformations (including MEC-quotients and automata-products), and algorithmic results for checking causality and computing quality measures like recall, coverage ratio, and f-score. The study delivers complexity bounds across settings: SPR checks are polynomial-time in fixed-cause cases, GPR checks are coNP-complete in general and NP-hard for some quality metrics, and ω-regular extensions rely on reductions to reachability problems with robust automata-based constructions. Overall, the work lays mathematical and algorithmic foundations for causal explanations in probabilistic nondeterministic systems with practical implications for verification, monitoring, and explainability.

Abstract

This work introduces a novel cause-effect relation in Markov decision processes using the probability-raising principle. Initially, sets of states as causes and effects are considered, which is subsequently extended to regular path properties as effects and then as causes. The paper lays the mathematical foundations and analyzes the algorithmic properties of these cause-effect relations. This includes algorithms for checking cause conditions given an effect and deciding the existence of probability-raising causes. As the definition allows for sub-optimal coverage properties, quality measures for causes inspired by concepts of statistical analysis are studied. These include recall, coverage ratio and f-score. The computational complexity for finding optimal causes with respect to these measures is analyzed.

Foundations of probability-raising causality in Markov decision processes

TL;DR

This paper develops a formal probabilistic causality framework for Markov decision processes by introducing probability-raising causes (SPR and GPR) under temporal priority constraints. It provides rigorous definitions, model-transformations (including MEC-quotients and automata-products), and algorithmic results for checking causality and computing quality measures like recall, coverage ratio, and f-score. The study delivers complexity bounds across settings: SPR checks are polynomial-time in fixed-cause cases, GPR checks are coNP-complete in general and NP-hard for some quality metrics, and ω-regular extensions rely on reductions to reachability problems with robust automata-based constructions. Overall, the work lays mathematical and algorithmic foundations for causal explanations in probabilistic nondeterministic systems with practical implications for verification, monitoring, and explainability.

Abstract

This work introduces a novel cause-effect relation in Markov decision processes using the probability-raising principle. Initially, sets of states as causes and effects are considered, which is subsequently extended to regular path properties as effects and then as causes. The paper lays the mathematical foundations and analyzes the algorithmic properties of these cause-effect relations. This includes algorithms for checking cause conditions given an effect and deciding the existence of probability-raising causes. As the definition allows for sub-optimal coverage properties, quality measures for causes inspired by concepts of statistical analysis are studied. These include recall, coverage ratio and f-score. The computational complexity for finding optimal causes with respect to these measures is analyzed.
Paper Structure (25 sections, 43 theorems, 154 equations, 18 figures, 1 table)

This paper contains 25 sections, 43 theorems, 154 equations, 18 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Markov decision processes
  4. MR-scheduler in MDPs without ECs
  5. MEC-quotient
  6. Automata and ω-regular languages
  7. Strict and global probability-raising causes
  8. Examples and simple properties of probability-raising causes
  9. Checking the existence of PR causes and the PR conditions
  10. Checking the strict probability-raising condition and the existence of causes
  11. Checking the global probability-raising condition
  12. Quality and optimality of causes
  13. Quality measures for causes
  14. Computation schemes for the quality measures for fixed cause set
  15. Quality-optimal probability-raising causes
  16. ...and 10 more sections

Key Result

Lemma 2.1

Consider an MDP $\mathcal{M}=(S,\mathit{Act},P,\mathsf{init})$ without end components. Then, for each scheduler $\mathfrak{S}$ for $\mathcal{M}$, there exists an MR-scheduler $\mathfrak{T}$ such that:

Figures (18)

  • Figure 1: A MC allowing for non-strict GPR causes
  • Figure 2: A MC with no PR cause
  • Figure 3: MDP $\mathcal{M}$ from Remark \ref{['rem:memory-needed']}
  • Figure 4: MDP $\mathcal{M}$ from Remark \ref{['rem:randomization-needed']}
  • Figure 5: MDP $\mathcal{M}$ from Remark \ref{['remark:action-causality']}
  • ...and 13 more figures

Theorems & Definitions (97)

  • Lemma 2.1: From general schedulers to MR-schedulers in MDPs without ECs
  • Lemma 2.2: Convex combination of MR-schedulers
  • proof
  • Definition 2.3: MEC-quotient of an MDP
  • Lemma 2.4: Correspondence of an MDP and its MEC-quotient
  • proof
  • Definition 3.1: Global and strict probability-raising cause (GPR/SPR cause)
  • Lemma 3.2: Singleton PR causes
  • Lemma 3.3
  • proof
  • ...and 87 more