| Popis: |
The complexity of modern computer and software systems still seems to grow exponentially, while the human user is widely left without explanations on how to understand these systems. One of the central tasks of current computer science therefore lies in the development of methods and tools to build such an understanding. A similar task is addressed by formal verification which gives various verifiable justifications for the functionality of a system. As these still only give knowledge that a system functions properly they only address a portion of the task to make systems easier to comprehend. It is widely believed that cause-effect reasoning plays an important role in forming human understanding of complex relations. Thus, there are already many accounts on causality in modern computer science. However, most of them are focusing on a form of backward looking actual causality. This variant of causality is concerned with actual events after their occurrence and tries to reason about causes mostly in a counterfactual manner. In this thesis we address a probabilistic form of causality which is forward looking by nature. As such, we define and discuss novel notions of probabilistic causes in discrete time Markov chains and Markov decision processes. For this we rely on two central principles of probabilistic causality. On one hand, the probability-raising principle states that a cause should raise the probability of its effect. On the other hand, temporal priority requires that a cause must occur before its effect. We build the mathematical and algorithmic foundations of our so called probability-raising causes. For this we work in a state-based setting where causes and effects are reachability properties of sets of states. In order to measure the predictive power of states we define quality-measures for which we interpret causes as binary classifiers. With these tools we address the algorithmic questions of checking cause-effect relations if both a cause candidate and an effect are given and finding quality-optimal causes if only the effect is given. We discuss possible extensions of this basic state-based framework to more general formulations of causes and effects as ω-regular properties.:Abstract 3 1 Introduction 7 1.1 Contributions and Outline ... ... ... ... ... ... ... ... ... .... . 15 1.2 Related Work ... ... ... ... ... ... ... ... ... ... ... ... ... 17 2 Preliminaries 21 2.1 Markov Decision Processes ... ... ... ... ... ... ... ... ... .... 22 2.1.1 Graph of an MDP ... ... ... ... ... ... ... ... ... .... . 22 2.1.2 Schedulers and Probability Measure ... ... ... ... ... ... ... 23 2.1.3 Maximal and Minimal Probabilities ... ... ... ... ... ... .... 25 2.1.4 Frequencies and Balance Equations ... ... ... ... ... ... ... 26 2.1.5 MR Scheduler in MDPs without ECs ... ... ... ... ... ... .... 26 2.1.6 MEC-Quotient ... ... ... ... ... ... ... ... ... ... .... 27 2.2 Automata and ω-Regular Languages ... ... ... ... ... ... ... .... 30 2.3 Probability-Raising Causality ... ... ... ... ... ... ... ... ... ... 31 3 Probability-Raising Causality in Markov Decision Processes 33 3.1 Setting and Definition ... ... ... ... ... ... ... ... ... ... .... 33 3.1.1 Related Work revisited ... ... ... ... ... ... ... ... .... . 38 3.2 Examples ... ... ... ... ... ... ... ... ... ... ... ... ... ... 42 3.2.1 Conceptual Examples ... ... ... ... ... ... ... ... ... ... 42 3.2.2 Racetrack MDP ... ... ... ... ... ... ... ... ... ... .... 47 3.3 Quality Measures for Probability-Raising Causes ... ... ... ... ... ... 52 3.3.1 PR Causes as Binary Classifiers in MDPs ... ... ... ... ... .... 53 3.3.2 Quality Measures for a given PR Cause ... ... ... ... ... .... . 54 4 Algorithmic Considerations 59 4.1 Checking the Probability-Raising Conditions ... ... ... ... ... ... ... 60 4.1.1 Canonical MDP for given Cause Set ... ... ... ... ... ... .... 61 4.1.2 Checking the SPR Condition and the Existence of PR Causes ... .... 72 4.1.3 Checking the GPR Condition ... ... ... ... ... ... ... .... . 77 4.2 Computing the Quality of a PR Cause ... ... ... ... ... ... ... .... 88 4.2.1 Max/Min Ratios for Disjoint Sets of Terminal States ... ... ... ... 92 4.3 Quality-Optimal Probability-Raising Causes ... ... ... ... ... ... .... 97 4.3.1 Quality-Optimal SPR Causes ... ... ... ... ... ... ... .... . 98 4.3.2 Quality-Optimal GPR Causes ... ... ... ... ... ... ... .... . 108 5 Variants of Probability-Raising Causality in MDPs 115 5.1 Probability-Raising Scheduler and Potential PR Causes ... ... ... ... ... 116 5.1.1 Checking for SPR Scheduler ... ... ... ... ... ... ... .... . 119 5.1.2 Checking for GPR Scheduler ... ... ... ... ... ... ... .... . 124 5.2 ω-Regular Effects - Reachability Causes ... ... ... ... ... ... ... ... 127 5.2.1 Checking Reachability Probability-Raising Causes ... ... ... .... . 128 5.2.2 Quality and Optimality of Reachability PR Causes ... ... ... .... . 133 5.3 ω-Regular Co-Safety Causes ... ... ... ... ... ... ... ... ... ... 137 5.3.1 Checking Co-Safety PR causes ... ... ... ... ... ... ... .... 139 5.3.2 Quality and Optimality of Co-Safety PR Causes ... ... ... ... ... 142 6 Conclusion 147 |
