Abstract

In this talk, I will (briefly) introduce the theory of actual causality as defined by Halpern and Pearl. This theory turns out to be extremely useful in various areas of computer science (and also, perhaps surprisingly, psychology) due to a good match between the results it produces and our intuition. I will outline the evolution of the definitions of actual causality and intuitive reasons for the many parameters in the definition using examples from formal verification. I will also introduce the definitions of responsibility and blame, which quantify the definition of causality.

We will look in more detail at the applications of causality to formal verification, namely, explanation of counter-examples, refinement of coverage metrics, and symbolic trajectory evaluation. It is interesting to note that explanation of counter-examples using the definition of actual causality is implemented in an industrial tool and produces results that are usually consistent with the users’ intuition, hence it is a popular and widely used feature of the tool.

Finally, I will briefly discuss recent applications of causality to legal reasoning and to understanding of political phenomena, and will conclude with outlining promising future directions.

The talk is based on many papers written by many people, and is not limited to my own research. The talk is reasonably self-contained.