Model Checking Causality

We present a novel modal language for causal reasoning and interpret it by means of a semantics in which causal information is represented using causal bases in propositional form. The language includes modal operators of conditional causal necessity where the condition is a causal change operation. We provide a succinct formulation of model checking for our language and a model checking procedure based on a polysize reduction to QBF. We illustrate the expressiveness of our language through some examples and show that it allows us to represent and to formally verify a variety of concepts studied in the field of explainable AI including abductive explanation, intervention and actual cause.

Authors

• Tiago de Lima CRIL, Univ Artois and CNRS, Lens, France
• Emiliano Lorini

Keywords

• Knowledge Representation and Reasoning: KRR: Causality
• Knowledge Representation and Reasoning: KRR: Knowledge representation languages