Counterfactual Causality in Real-Time Systems
Felix Jahn
Verifying specifications of computer systems is a well-explored task addressed, for instance, by model checking. Understanding a negative model checking result is, however, difficult. In such an instance, a counterexample witnessing the violation will be returned but yields only limited insights for debugging. A promising technique to foster understanding of counterexamples is to generate explanations based on causal analyses. For real-time systems – which have to satisfy crucial real-time constraints and are increasingly deployed in various safety-critical contexts like traffic, manufacturing, or healthcare – causal analyses, however, are especially hard: not only the performed actions of the systems but also their real-time behavior contributes to the overall system behavior. In this thesis, we present multiple notions of counterfactual causality for real-time systems that consider both actions and real-time behavior for potential causes. This then yields precise explanations for observed effects in the executions of the systems, which we model as timed automata. Our definitions are based on the seminal conceptual work on causality by Halpern and Pearl. We adapt their ideas for counterfactual reasoning to the real-time setting by representing counterfactual executions using counterfactual trace automata. This enables us to define progressively more refined causality notions and to thereby adopt different perspectives on the timing behavior of real-time systems. We demonstrate the destined notions on numerous examples, present some basic theoretical properties, and provide algorithms for checking computing causal relationships. Furthermore, we analyze the complexity of both problems, which we show to be EXPSPACE-complete. Lastly, we report on the implementation of a Python tool for checking and computing causes for real-time systems modeled in Uppaal, enabling an automated explanation of counterexamples.
Master Thesis.